Please use this identifier to cite or link to this item: http://hdl.handle.net/10889/10917
Title: Elementary theorem-proving applications of the OTTER automated deduction system in structural mechanics
Other Titles: Στοιχειώδεις εφαρμογές αποδείξεως θεωρημάτων του συστήματος αυτόματης εξαγωγής συμπερασμάτων OTTER στη μηχανική των κατασκευών
Authors: Ioakimidis, Nikolaos
Keywords: Automated theorem proving
Automated reasoning
Automated deduction
Predicate logic
Formal proofs
OTTER
Beams
Elastic foundations
Structures
Trusses
Keywords (translated): Αυτόματη απόδειξη θεωρημάτων
Αυτόματη συλλογιστική
Αυτόματη εξαγωγή συμπερασμάτων
Κατηγορηματική λογική
Τυπικές αποδείξεις
OTTER
Δοκοί
Ελαστικές θεμελιώσεις
Κατασκευές
Δικτυώματα
Abstract: 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.
Abstract (translated): Παρουσιάζονται τέσσερις στοιχειώδεις εφαρμογές στη μηχανική των κατασκευών του διάσημου προγράμματος υπολογιστή OTTER (Organized Techniques for Theorem Proving and Effective Research) του McCune για την αυτόματη εξαγωγή συμπερασμάτων/απόδειξη θεωρημάτων. Αυτές οι εφαρμογές αφορούν (i) σε συμπεράσματα για τη στήριξη και τις συνοριακές συνθήκες στα άκρα απλής δοκού, (ii) στο στοιχειώδες πρόβλημα των αντιδράσεων στα άκρα απλής δοκού, (iii) στο γραμμικό συνδυασμό των τεσσάρων στοιχειωδών λύσεων της ομογενούς συνήθους διαφορικής εξισώσεως τετάρτης τάξεως δοκού σε ελαστική θεμελίωση και (iv) στην τυπική απόδειξη της απουσίας αξονικής φορτίσεως σε τέσσερις ράβδους ενός απλού δικτυώματος. Με τη χρήση του OTTER ή ενός ανταγωνιστικού προγράμματος αυτόματης εξαγωγής συμπερασμάτων/αποδείξεως θεωρημάτων μπορούν επίσης να μελετηθούν και άλλα προβλήματα της μηχανικής των κατασκευών που μπορούν να διατυπωθούν τυπικά σαν απλά θεωρήματα (δηλαδή μπορούν να αποδειχθούν τα σχετικά θεωρήματα). Από πρακτική άποψη τα παρόντα αποτελέσματα στοχεύουν στην επίδειξη της πιθανής χρησιμότητας τεχνικών αυτόματης εξαγωγής συμπερασμάτων/αποδείξεως θεωρημάτων στη μηχανική των κατασκευών σαν ένα ενδεχομένως πρόσθετο και ίσως εν μέρει ενδιαφέρον εργαλείο πέρα από τα πολύ γνωστά εργαλεία των αριθμητικών και συμβολικών υπολογισμών, του σχεδιασμού με τη βοήθεια υπολογιστή, των έμπειρων συστημάτων, κλπ. ειδικά κατά τη διάρκεια της επαληθεύσεως αποτελεσμάτων μη επαρκώς αποδεδειγμένων ή απλά εικαζόμενων (εικασίες) από το δομικό μηχανικό. Αφετέρου, από θεωρητική άποψη τα παρόντα αποτελέσματα επιχειρούν μια γενίκευση των τεχνικών αποδείξεως θεωρημάτων από τα καθαρά και εφαρμοσμένα μαθηματικά στη μηχανική των κατασκευών. Συζητούνται επίσης σύντομα και παραπέρα δυνατότητες της μεθόδου.
Appears in Collections:Γενικό Τμήμα (Τεχνικές Αναφορές)

Files in This Item:
File Description SizeFormat 
TR-2001-O7.pdf233.59 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons