The analysis and partial synthesis of truss structures via theorem proving

A use of theorem proving for the analysis and partial synthesis of truss structures is presented. The behavior of a truss structure is modeled as the set union of the behavior of its constituent components where the behavior of each component is modeled by a set of constraints. This component/constraint model is formally represented by a set of axioms using predicate logic. The axioms are then used toanalyze and partiallysynthesize truss structures via theorem proving.Constraint logic programming is identified as a suitable implementation vehicle for the analysis and partial synthesis of truss structures via theorem proving. Several important implications of the formulation for structural design automation, data base integrity, and parallel processing are discussed.