Elementary engineering mechanics applications of the OTTER automated reasoning system

• Main Author: Ioakimidis, Nikolaos
• Other Authors: Ιωακειμίδης, Νικόλαος
• Format: Technical Report
• Language: English
• Published: 2018
• Subjects: Automated proofs; Automated reasoning; Automated deduction; Formal proofs; Predicate logic; OTTER; Engineering mechanics; Fracture mechanics; Stress intensity factors; Cracks; Structural mechanics; Beams; Αυτοματοποιημένες αποδείξεις; Αυτοματοποιημένη συλλογιστική; Αυτοματοποιημένη εξαγωγή συμπερασμάτων; Τυπικές αποδείξεις; Κατηγορηματική λογική; Μηχανική για μηχανικούς; Θραυστομηχανική; Συντελεστές εντάσεως τάσεων; Ρωγμές; Μηχανική των κατασκευών; Δοκοί

The famous resolution-based McCune's OTTER automated reasoning (or automated deduction) program has been used for the logical proof of elementary statements in mechanics on the basis of hypotheses either of general or of particular validity. Three such simple applications concerning fracture and structural mechanics in applied mechanics are described and the related OTTER's complete input files and formal proofs are provided in all three cases. In the second of these applications, hypotheses including the disjunction of two (positive) possibilities are included in the related set, whereas in the third of these applications algebraic equality hypotheses are also present. The aim of these results is to attempt to use a very popular automated reasoning program (mainly being employed for formal proofs in pure mathematics and logic) in applied mechanics as a somewhat different possibility to the use of Prolog and expert systems and, in principle, with more general acceptable input clauses as well as a much more powerful reasoning–inference engine than Prolog. It is hoped that in the future there will become possible to combine numerical, symbolic and graphical computational facilities, already offered (simultaneously) by classical computer algebra systems (such as Maple and Mathematica), with automated reasoning systems (such as OTTER) in the same computational environment. Presently, the present results simply encourage the use of formal proofs (so popular in mathematics and logic) also in engineering mechanics, a fact already achieved here with moderate success with the help of OTTER. The encouragement to the axiomatization of simple engineering mechanics particular areas, although not attempted here, nevertheless seems also to constitute a possible by-product of the present approach, which seems to be new.