Η παρούσα διπλωματική εργασία έχει ως σκοπό να κάνει μια σύνδεση μεταξύ της ιστορικής εξέλιξης των αποδεικτικών μαθηματικών μεθόδων, κυρίως αυτών της Γεωμετρίας, με τα σημερινά επιτεύγματα της τεχνολογίας στον τομέα των υπολογιστικών προγραμμάτων και εφαρμογών που βοηθούν στην κατανόηση και επαλήθευσή της, καθώς και με ποιο τρόπο η εξέλιξη της προτασιακής και κατηγορηματικής λογικής συνέβαλε στην ανάπτυξη των προγραμμάτων αυτών.
Στο πρώτο μέρος, μέσα από μια σύντομη αναδρομή στην εξέλιξη των αποδεικτικών μεθόδων, αναδεικνύεται η σημασία της απόδειξης στα μαθηματικά και ειδικότερα στον κλάδο της Γεωμετρίας, καθώς και η αναγκαιότητά της για επιβεβαίωση των εμπειρικών γεωμετρικών πειραμάτων και πρακτικών ιδεών. Η προαναφερθείσα σύνδεση γίνεται μέσω μιας παρουσίασης των λογισμικών Δυναμικής Γεωμετρίας, τα οποία χρησιμοποιούνται ως νέες τεχνολογίες στον τομέα της εκπαίδευσης, τονίζοντας τη σημαντική βοήθεια που δίνουν στην οπτική αναπαράσταση των θεωρητικών γεωμετρικών προτάσεων και ειδικότερα εκείνων που ενσωματώνουν αυτόματους ελεγκτές αποδείξεων, καθώς και των βημάτων προόδου που έχουν γίνει στον τομέα παραγωγής αυτόματων αποδείξεων.
Στο δεύτερο μέρος, παρουσιάζεται μια προσέγγιση υλοποίησης αυτόματης παραγωγής αποδείξεων βασικών θεωρημάτων που αφορούν κυρίως τις σχέσεις μεταξύ γωνιών. Αυτή επιτυγχάνεται μέσω παράθεσης των θεωρημάτων της Ευκλείδειας Γεωμετρίας που αφορούν τις σχέσεις ευθειών, ευθυγράμμων τμημάτων και γωνιών, και ενοποίησής τους στην υλοποίηση με τον αποδείκτη Prover9 που θα χρησιμοποιηθεί. Οι συγκεκριμένες μέθοδοι επηρεάζουν δραστικά τον τρόπο παραγωγής εναλλακτικών μονοπατιών απόδειξης και αποτελούν σημαντικό κεφάλαιο στον τομέα της εκπαίδευσης αλλά και της τεχνητής νοημοσύνης. Πραγματοποιείται επίσης μια αναλυτική παρουσίαση του συγκεκριμένου εργαλείου. Τέλος, παρατίθενται τα συμπεράσματα που απορρέουν από την υλοποίηση αυτή, καθώς και οι προτεινόμενες προεκτάσεις και μετέπειτα ενέργειες που μπορούν να επιτευχθούν μέσω αυτής.
This thesis aims at linking the historical development of mathematical proving methods, especially those of Geometry, with the current achievements of technology in the field of computer programs and applications, as well as with the way the development of the propositional and categorical logic contributed to the development of these programs.
In the first part, through a brief review of the evolution of the evidence methods, the importance of evidence in mathematics and especially in the field of Geometry, as well as its necessity to confirm empirical geometric experiments and practical ideas, is highlighted. The connection is made through a presentation of the Dynamic Geometry software, which is used as a new technology in the field of education, emphasizing to the important help that gives the visual representation of theoretical geometric proposals, as well as the progress steps which have been made in the field of automatic proofs.
In the second part, an approach for the realization of automatic production of proofs of basic theorems is presented, mainly concerning angles equality. This is achieved by presenting the theorems of Euclidean Geometry concerning the relations between lines, segments and angles, and trying to prove them through Prover9. These methods have a dramatic impact on how to produce alternative proof paths and are an important chapter in the field of education and artificial intelligence. There is also an extended presentation of this tool. Finally, the conclusions drawn from this implementation, as well as the proposed extensions and subsequent actions that can be reached through this implementation, are presented.
Αποδεικτικές μέθοδοι στην Ευκλείδεια Γεωμετρία και αυτόματοι αποδείκτες θεωρημάτων