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.
(EL)
Το διάσημο πρόγραμμα αυτoματοποιημένης συλλογιστικής (ή αυτοματοποιημένης εξαγωγής συμπερασμάτων) OTTER του McCune, που βασίζεται στην ανάλυση (resolution), χρησιμοποιήθηκε για τη λογική απόδειξη στοιχειωδών προτάσεων στη μηχανική με βάση υποθέσεις είτε γενικής είτε ειδικής ισχύος. Περιγράφονται τρεις τέτοιες απλές εφαρμογές που αφορούν στη θραυστομηχανική και στη μηχανική των κατασκευών στην εφαρμοσμένη μηχανική και παρουσιάζονται τα σχετικά πλήρη αρχεία εισόδου του OTTER και οι σχετικές τυπικές αποδείξεις και στις τρεις περιπτώσεις. Στη δεύτερη από αυτές τις εφαρμογές περιλαμβάνονται στο σχετικό σύνολο υποθέσεις που περιλαμβάνουν τη διάζευξη δύο (θετικών) δυνατοτήτων, ενώ στην τρίτη από αυτές τις εφαρμογές είναι επίσης παρούσες αλγεβρικές υποθέσεις σε μορφή εξισώσεων. Ο στόχος αυτών των αποτελεσμάτων είναι να επιχειρήσουμε τη χρήση ενός πολύ δημοφιλούς προγράμματος αυτοματοποιημένης συλλογιστικής (που χρησιμοποιείται κυρίως σε τυπικές αποδείξεις στα καθαρά μαθηματικά και στη λογική) στην εφαρμοσμένη μηχανική σαν μια κάπως διαφορετική δυνατότητα από τη χρήση της Prolog και των έμπειρων συστημάτων και καταρχήν με πιο γενικές αποδεκτές προτάσεις εισόδου όπως επίσης και με μια πολύ πιο ισχυρή από την Prolog μηχανή συλλογιστικής–συμπερασμάτων. Ελπίζεται ότι στο μέλλον θα καταστεί δυνατός ο συνδυασμός αριθμητικών, συμβολικών και γραφικών υπολογιστικών δυνατοτήτων, που ήδη προσφέρονται (ταυτόχρονα) από κλασικά συστήματα υπολογιστικής άλγεβρας (όπως το Maple και το Mathematica), με αυτοματοποιημένα συστήματα συλλογιστικής (όπως το OTTER) στο ίδιο υπολογιστικό περιβάλλον. Επί του παρόντος τα παρόντα αποτελέσματα απλά ενθαρρύνουν τη χρήση τυπικών αποδείξεων (τόσο δημοφιλών στα μαθηματικά και στη λογική) επίσης στη μηχανική για μηχανικούς, ένα γεγονός που ήδη επιτεύχθηκε εδώ με μέτρια επιτυχία με τη βοήθεια του OTTER. H ενθάρρυνση της αξιοματικοποιήσεως απλών ειδικών περιοχών της μηχανικής για μηχανικούς, αν και δεν επιχειρείται εδώ, εντούτοις φαίνεται να αποτελεί επίσης ένα πιθανό παραπροϊόν της παρούσας μεθόδου, η οποία φαίνεται να είναι καινούργια.
(EL)
Πανεπιστήμιο Πατρών
