Αξιολόγηση και βελτίωση παρουσίασης αποδείξεων Ευκλείδειας Γεωμετρίας που παράγονται από αποδείκτες

  1. MSc thesis
  2. ΖΑΠΠΑΣ, ΝΙΚΟΛΑΟΣ
  3. Μεταπτυχιακή Εξειδίκευση στα Πληροφοριακά Συστήματα (ΠΛΣ)
  4. 21 September 2019 [2019-09-21]
  5. Ελληνικά
  6. 71
  7. ΚΑΛΛΕΣ, ΔΗΜΗΤΡΙΟΣ
  8. Αποδείκτες | Prover | Γεωμετρία | Geometry | Αυτόματος | Automated | Prover9 | ATP
  9. 3
  10. 1
  11. 8
  12. 17 Εικόνες
    • Σκοπός της παρούσας διπλωματικής εργασίας ήταν να βελτιώσει την αναγνωσιμότητα μιας γεωμετρικής απόδειξης ενός προβλήματος γεωμετρίας που παράγεται από έναν αυτόματο αποδείκτη θεωρημάτων. Αυτό έγινε μειώνοντας το μέγεθος των αποδείξεων ως προς το μήκος τους, το πλάτος τους, τον αριθμό των παραγόμενων προτάσεων και τον χρόνο παραγωγής τους. Η εργασία αποτελείται από δύο μέρη. Στο πρώτο μέρος έχουμε την ανάγνωση και δημιουργία περιλήψεων από εργασίες που έγιναν σε διάφορα Πανεπιστήμια ή από άρθρα που έχουν δημοσιευτεί από εταιρείες λογισμικού ή από μεμονωμένους επιστήμονες. Τα αντικείμενα των εργασιών ή άρθρων είναι τα εξής: η βελτίωση της γεωμετρικής απόδειξης αυτόματων αποδεικτών, η αυτόματη ανίχνευση ομοιότητας σε δύο σύνολα λέξεων και η ανάλυση στην αυτοματοποιημένη συλλογιστική. Με τις περιλήψεις αυτές κάνουμε φανερό το ενδιαφέρον της παγκόσμιας κοινότητας για τους αυτόματους αποδείκτες και βλέπουμε τα βήματα που έχουν γίνει στην κατεύθυνση αυτή. Στο δεύτερο μέρος, έχουμε την μελέτη τρόπων βελτίωσης αποδείξεων δύο απλών αλλά βασικών θεωρημάτων που είναι απαραίτητα για την απόδειξη ενός συγκεκριμένου γεωμετρικού προβλήματος. Δεδομένου πως οι αποδείξεις παράγονται με χρήση του αποδείκτη Prover9, οι βελτιώσεις που επιδιώκουμε υλοποιούνται είτε αλλάζοντας τιμές σε κάποιες παραμέτρους του αποδείκτη Prover9 είτε αλλάζοντας τα δεδομένα ή τα ζητούμενα των θεωρημάτων.
    • The purpose of this diploma thesis was to improve the readability of a geometric proof of a geometry problem produced by an automated theorem prover. This was done by reducing the size of proofs in terms of length, width, number of sentences produced, and time of production. The work consists of two parts. In the first part we have read and summarize work done in various Universities or articles published by Software Companies or by individual scientists. The objects of the papers or articles are: the improvement of the geometric proof that is produced from automated theorem provers, the automatic detection of similarity in two sets of words and the analysis in automated reasoning. With these summaries, we make clear the interest of the global community for automated theorem provers and we see the steps that have been taken in this direction. In the second part, we study ways to improve evidence of two simple but basic theorems necessary to prove a specific geometric problem. As the proof is produced using Prover9 (automated theorem prover), the improvements we seek are made either by changing values in some parameters of Prover9 or by changing the data or the conclusion of theorems.
  14. Items in Apothesis are protected by copyright, with all rights reserved, unless otherwise indicated.