Please use this identifier to cite or link to this item: http://hdl.handle.net/10889/10919
Title: Elementary engineering mechanics applications of the OTTER automated reasoning system
Other Titles: Στοιχειώδεις εφαρμογές στη μηχανική για μηχανικούς του συστήματος αυτοματοποιημένης συλλογιστικής OTTER
Authors: Ioakimidis, Nikolaos
Keywords: Automated proofs
Automated reasoning
Automated deduction
Formal proofs
Predicate logic
OTTER
Engineering mechanics
Fracture mechanics
Stress intensity factors
Cracks
Structural mechanics
Beams
Keywords (translated): Αυτοματοποιημένες αποδείξεις
Αυτοματοποιημένη συλλογιστική
Αυτοματοποιημένη εξαγωγή συμπερασμάτων
Τυπικές αποδείξεις
Κατηγορηματική λογική
OTTER
Μηχανική για μηχανικούς
Θραυστομηχανική
Συντελεστές εντάσεως τάσεων
Ρωγμές
Μηχανική των κατασκευών
Δοκοί
Abstract: 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.
Abstract (translated): Το διάσημο πρόγραμμα αυτoματοποιημένης συλλογιστικής (ή αυτοματοποιημένης εξαγωγής συμπερασμάτων) OTTER του McCune, που βασίζεται στην ανάλυση (resolution), χρησιμοποιήθηκε για τη λογική απόδειξη στοιχειωδών προτάσεων στη μηχανική με βάση υποθέσεις είτε γενικής είτε ειδικής ισχύος. Περιγράφονται τρεις τέτοιες απλές εφαρμογές που αφορούν στη θραυστομηχανική και στη μηχανική των κατασκευών στην εφαρμοσμένη μηχανική και παρουσιάζονται τα σχετικά πλήρη αρχεία εισόδου του OTTER και οι σχετικές τυπικές αποδείξεις και στις τρεις περιπτώσεις. Στη δεύτερη από αυτές τις εφαρμογές περιλαμβάνονται στο σχετικό σύνολο υποθέσεις που περιλαμβάνουν τη διάζευξη δύο (θετικών) δυνατοτήτων, ενώ στην τρίτη από αυτές τις εφαρμογές είναι επίσης παρούσες αλγεβρικές υποθέσεις σε μορφή εξισώσεων. Ο στόχος αυτών των αποτελεσμάτων είναι να επιχειρήσουμε τη χρήση ενός πολύ δημοφιλούς προγράμματος αυτοματοποιημένης συλλογιστικής (που χρησιμοποιείται κυρίως σε τυπικές αποδείξεις στα καθαρά μαθηματικά και στη λογική) στην εφαρμοσμένη μηχανική σαν μια κάπως διαφορετική δυνατότητα από τη χρήση της Prolog και των έμπειρων συστημάτων και καταρχήν με πιο γενικές αποδεκτές προτάσεις εισόδου όπως επίσης και με μια πολύ πιο ισχυρή από την Prolog μηχανή συλλογιστικής–συμπερασμάτων. Ελπίζεται ότι στο μέλλον θα καταστεί δυνατός ο συνδυασμός αριθμητικών, συμβολικών και γραφικών υπολογιστικών δυνατοτήτων, που ήδη προσφέρονται (ταυτόχρονα) από κλασικά συστήματα υπολογιστικής άλγεβρας (όπως το Maple και το Mathematica), με αυτοματοποιημένα συστήματα συλλογιστικής (όπως το OTTER) στο ίδιο υπολογιστικό περιβάλλον. Επί του παρόντος τα παρόντα αποτελέσματα απλά ενθαρρύνουν τη χρήση τυπικών αποδείξεων (τόσο δημοφιλών στα μαθηματικά και στη λογική) επίσης στη μηχανική για μηχανικούς, ένα γεγονός που ήδη επιτεύχθηκε εδώ με μέτρια επιτυχία με τη βοήθεια του OTTER. H ενθάρρυνση της αξιοματικοποιήσεως απλών ειδικών περιοχών της μηχανικής για μηχανικούς, αν και δεν επιχειρείται εδώ, εντούτοις φαίνεται να αποτελεί επίσης ένα πιθανό παραπροϊόν της παρούσας μεθόδου, η οποία φαίνεται να είναι καινούργια.
Appears in Collections:Γενικό Τμήμα (Τεχνικές Αναφορές)

Files in This Item:
File Description SizeFormat 
TR-1998-O1.pdf161.54 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons