Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων
Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (Automatic Theorem Proving Systems-ATP Systems) είναι συστήματα βασισμένα στη λογική πρώτης τάξεως, τα οποία μπορούν από ένα σύνολο λογικών προτάσεων να συνάγουν την αλήθεια μιας δεδομένης λογικής πρότασης με αυτόματο τρόπο. Η διαδικασία της απόδειξ...
| Κύριος συγγραφέας: | |
|---|---|
| Άλλοι συγγραφείς: | |
| Μορφή: | Thesis |
| Γλώσσα: | Greek |
| Έκδοση: |
2010
|
| Θέματα: | |
| Διαθέσιμο Online: | http://nemertes.lis.upatras.gr/jspui/handle/10889/2703 |
| id |
nemertes-10889-2703 |
|---|---|
| record_format |
dspace |
| spelling |
nemertes-10889-27032022-09-05T20:21:47Z Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων Γριβοκωστοπούλου, Φωτεινή Χατζηλυγερούδης, Ιωάννης Σγράμπας, Κυριάκος Βουτσινάς, Βασίλειος Grivokostopoulou, Foteini Αυτόματη απόδειξη θεωρημάτων Βιβλιοθήκη TPTP Στρατηγικές ελέγχου Automatic theorem proving TPTP library Control strategies 511.3 Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (Automatic Theorem Proving Systems-ATP Systems) είναι συστήματα βασισμένα στη λογική πρώτης τάξεως, τα οποία μπορούν από ένα σύνολο λογικών προτάσεων να συνάγουν την αλήθεια μιας δεδομένης λογικής πρότασης με αυτόματο τρόπο. Η διαδικασία της απόδειξης στα περισσότερα ΣΑΑΘ στηρίζεται στην αρχή της επίλυσης, τον ισχυρότερο κανόνα λογικής εξαγωγής συμπερασμάτων, και την αντίφαση της επίλυσης, μια διαδικασία που εξασφαλίζει την ορθότητα των συμπερασμάτων. Ο ACT-P είναι ένα ΣΑΑΘ που στηρίζεται στην αρχή της επίλυσης και την αντίφαση της επίλυσης, γραμμένο στο εργαλείο GCLISP Developer 5.0 της Gold-Hill, και διαθέτει μια βιβλιοθήκη γνωστών στρατηγικών ελέγχου της διαδικασίας απόδειξης, προσφέροντας τη δυνατότητα στον χρήστη να ορίσει κάθε φορά ένα (κατάλληλο) συνδυασμό στρατηγικών. Στην εργασία αυτή έγινε κατ’ αρχήν μεταφορά του ACT-P σε LispWorks, ένα δυναμικότερο εργαλείο ανάπτυξης εφαρμογών σε Lisp. Επιπλέον, ο χρήστης μέσω του νέου παραθυρικού περιβάλλοντος μπορεί να βλέπει δυο διαφορετικές λύσεις του ίδιου προβλήματος, τη συνοπτική και αναλυτική λύση. Στη συνέχεια, έγινε έλεγχος της καλής λειτουργίας του ACT-P και των στρατηγικών του μέσω δοκιμών με προβλήματα που προέρχονται από την TPTP (Thousands of Problems for Theorem Provers), μια γνωστή βιβλιοθήκη προβλημάτων για ΣΣΑΘ συστήματα στο Διαδίκτυο, και έγιναν οι απαραίτητες διορθώσεις έτσι ώστε να επιλύει προβλήματα από διάφορες κατηγορίες προβλημάτων της βιβλιοθήκης TPTP. Τέλος, έγινε μια μελέτη χρήσης διαφόρων συνδυασμών στρατηγικών ελέγχου για διάφορα προβλήματα της TPTP και εξήχθησαν χρήσιμα συμπεράσματα για την καταλληλότητά τους και την αποδοτικότητά τους σε σχέση με το είδος των προβλημάτων. Automatic Theorem Proving Systems (ATP Systems) are based on First Order Logic (FOL) and are able to automatically prove the truth of logical sentence. The proof procedure in most ATP Systems uses the resolution principle which is the strongest existing inference rule, and the resolution refutation process which ensure soundeness of the conclusion. The ACT-P is an ATP System which uses the resolution principle and the resolution refutation and it is written in GCLISP Developer 5.0 of Gold-Hill. ACT-P has a library of strategies to control the proof process, and gives users the ability to assign to specify a suitable combination of strategies. In this dissertation a new window based interface is developed for ACTP in Lispworks, which is a powerful tool for developing Lisp applications. The interface gives to the user a more thorough view of the solving process. Moreover, the user can see two different solutions of the problem, the brief and the analytic one. In addition, the functionality and the strategies of ACTP were tested on problems from the TPTP (Thousands of Problems for Theorem Provers) which is a known library of problems for ATP Systems on the web. ACTP has been improved so as to solve problems from various categories of the TPTP library. Finally, different strategy combinations for solving problems from various categories of TPTP library were studied, leading to useful conclusions about the suitability and the performance of the different combinations depending on the problems. 2010-03-15T09:08:13Z 2010-03-15T09:08:13Z 2009-12-15 2010-03-15T09:08:13Z Thesis http://nemertes.lis.upatras.gr/jspui/handle/10889/2703 gr Η ΒΥΠ διαθέτει αντίτυπο της διατριβής σε έντυπη μορφή στο βιβλιοστάσιο διδακτορικών διατριβών που βρίσκεται στο ισόγειο του κτιρίου της. 0 application/pdf |
| institution |
UPatras |
| collection |
Nemertes |
| language |
Greek |
| topic |
Αυτόματη απόδειξη θεωρημάτων Βιβλιοθήκη TPTP Στρατηγικές ελέγχου Automatic theorem proving TPTP library Control strategies 511.3 |
| spellingShingle |
Αυτόματη απόδειξη θεωρημάτων Βιβλιοθήκη TPTP Στρατηγικές ελέγχου Automatic theorem proving TPTP library Control strategies 511.3 Γριβοκωστοπούλου, Φωτεινή Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| description |
Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (Automatic Theorem Proving Systems-ATP Systems) είναι συστήματα βασισμένα στη λογική πρώτης τάξεως, τα οποία μπορούν από ένα σύνολο λογικών προτάσεων να συνάγουν την αλήθεια μιας δεδομένης λογικής πρότασης με αυτόματο τρόπο. Η διαδικασία της απόδειξης στα περισσότερα ΣΑΑΘ στηρίζεται στην αρχή της επίλυσης, τον ισχυρότερο κανόνα λογικής εξαγωγής συμπερασμάτων, και την αντίφαση της επίλυσης, μια διαδικασία που εξασφαλίζει την ορθότητα των συμπερασμάτων.
Ο ACT-P είναι ένα ΣΑΑΘ που στηρίζεται στην αρχή της επίλυσης και την αντίφαση της επίλυσης, γραμμένο στο εργαλείο GCLISP Developer 5.0 της Gold-Hill, και διαθέτει μια βιβλιοθήκη γνωστών στρατηγικών ελέγχου της διαδικασίας απόδειξης, προσφέροντας τη δυνατότητα στον χρήστη να ορίσει κάθε φορά ένα (κατάλληλο) συνδυασμό στρατηγικών.
Στην εργασία αυτή έγινε κατ’ αρχήν μεταφορά του ACT-P σε LispWorks, ένα δυναμικότερο εργαλείο ανάπτυξης εφαρμογών σε Lisp. Επιπλέον, ο χρήστης μέσω του νέου παραθυρικού περιβάλλοντος μπορεί να βλέπει δυο διαφορετικές λύσεις του ίδιου προβλήματος, τη συνοπτική και αναλυτική λύση.
Στη συνέχεια, έγινε έλεγχος της καλής λειτουργίας του ACT-P και των στρατηγικών του μέσω δοκιμών με προβλήματα που προέρχονται από την TPTP (Thousands of Problems for Theorem Provers), μια γνωστή βιβλιοθήκη προβλημάτων για ΣΣΑΘ συστήματα στο Διαδίκτυο, και έγιναν οι απαραίτητες διορθώσεις έτσι ώστε να επιλύει προβλήματα από διάφορες κατηγορίες προβλημάτων της βιβλιοθήκης TPTP.
Τέλος, έγινε μια μελέτη χρήσης διαφόρων συνδυασμών στρατηγικών ελέγχου για διάφορα προβλήματα της TPTP και εξήχθησαν χρήσιμα συμπεράσματα για την καταλληλότητά τους και την αποδοτικότητά τους σε σχέση με το είδος των προβλημάτων. |
| author2 |
Χατζηλυγερούδης, Ιωάννης |
| author_facet |
Χατζηλυγερούδης, Ιωάννης Γριβοκωστοπούλου, Φωτεινή |
| format |
Thesis |
| author |
Γριβοκωστοπούλου, Φωτεινή |
| author_sort |
Γριβοκωστοπούλου, Φωτεινή |
| title |
Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| title_short |
Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| title_full |
Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| title_fullStr |
Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| title_full_unstemmed |
Βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| title_sort |
βελτίωση και αξιοποίηση αποδείκτη θεωρημάτων |
| publishDate |
2010 |
| url |
http://nemertes.lis.upatras.gr/jspui/handle/10889/2703 |
| work_keys_str_mv |
AT gribokōstopoulouphōteinē beltiōsēkaiaxiopoiēsēapodeiktētheōrēmatōn |
| _version_ |
1771297291346378752 |
