Elementary theorem-proving applications of the OTTER automated deduction system in structural mechanics

• Κύριος συγγραφέας: Ioakimidis, Nikolaos
• Άλλοι συγγραφείς: Ιωακειμίδης, Νικόλαος
• Μορφή: Technical Report
• Γλώσσα: English
• Έκδοση: 2018
• Θέματα: Automated theorem proving; Automated reasoning; Automated deduction; Predicate logic; Formal proofs; OTTER; Beams; Elastic foundations; Structures; Trusses; Αυτόματη απόδειξη θεωρημάτων; Αυτόματη συλλογιστική; Αυτόματη εξαγωγή συμπερασμάτων; Κατηγορηματική λογική; Τυπικές αποδείξεις; Δοκοί; Ελαστικές θεμελιώσεις; Κατασκευές; Δικτυώματα

Four elementary applications of the famous McCune's OTTER (Organized Techniques for Theorem Proving and Effective Research) automated deduction/theorem-proving computer program in structural mechanics are presented. These applications concern (i) conclusions on the support and boundary conditions at the ends of a simple beam, (ii) the elementary problem of the reactions at the ends of a simple beam, (iii) the linear combination of the four elementary solutions of the fourth-order homogeneous ordinary differential equation of a beam on an elastic foundation and (iv) the formal proof of the lack of axial loading in four bars of a simple truss. Additional problems of structural mechanics formally stated as simple theorems can also be studied (i.e., the related theorems can be proved) by using OTTER or a competitive automated deduction/theorem-proving program. From the practical point of view the present results aim at the illustration of the possible usefulness of automated deduction/theorem-proving techniques is structural mechanics as a potentially additional and, maybe, partially interesting tool beyond the well-known tools of numerical and symbolic computations, computer-aided design, expert systems, etc. especially during the verification of results not sufficiently formally established or just guessed by the structural engineer (conjectures). On the other hand, from the theoretical point of view, the present results attempt a generalization of theorem-proving techniques from pure and applied mathematics to structural mechanics. Further possibilities of the method are also discussed in brief.