Please use this identifier to cite or link to this item: http://hdl.handle.net/10889/2703
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorΧατζηλυγερούδης, Ιωάννης-
dc.contributor.authorΓριβοκωστοπούλου, Φωτεινή-
dc.contributor.otherGrivokostopoulou, Foteini-
dc.date.accessioned2010-03-15T09:08:13Z-
dc.date.available2010-03-15T09:08:13Z-
dc.date.copyright2009-12-15-
dc.date.issued2010-03-15T09:08:13Z-
dc.identifier.urihttp://nemertes.lis.upatras.gr/jspui/handle/10889/2703-
dc.description.abstractΤα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (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 και εξήχθησαν χρήσιμα συμπεράσματα για την καταλληλότητά τους και την αποδοτικότητά τους σε σχέση με το είδος των προβλημάτων.en
dc.language.isogren
dc.relation.isformatofΗ ΒΥΠ διαθέτει αντίτυπο της διατριβής σε έντυπη μορφή στο βιβλιοστάσιο διδακτορικών διατριβών που βρίσκεται στο ισόγειο του κτιρίου της.en
dc.rights0en
dc.subjectΑυτόματη απόδειξη θεωρημάτωνen
dc.subjectΒιβλιοθήκη TPTPen
dc.subjectΣτρατηγικές ελέγχουen
dc.subject.ddc511.3en
dc.titleΒελτίωση και αξιοποίηση αποδείκτη θεωρημάτωνen
dc.typeThesisen
dc.contributor.committeeΣγράμπας, Κυριάκος-
dc.contributor.committeeΒουτσινάς, Βασίλειος-
dc.description.translatedabstractAutomatic 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.en
dc.subject.alternativeAutomatic theorem provingen
dc.subject.alternativeTPTP libraryen
dc.subject.alternativeControl strategiesen
dc.degreeΜεταπτυχιακή Εργασίαen
Appears in Collections:Τμήμα Μαθηματικών (ΜΔΕ)

Files in This Item:
File Description SizeFormat 
Grivokostopoulou_Foteini.pdf2.9 MBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons