Seminar
Abstract
Η κατασκευή αποδείξεων μέσω υπολογιστή γίνεται με τη χρήση ειδικών εργαλείων που ονομάζονται proof assistants. Η πρόοδος στην τεχνολογία αιχμής των proof assistants ειναι ραγδαια. Παρ'όλ'αυτά, η διαδικασία κατασκευής των απαιτούμενων αποδείξεων είναι εξαιρετικά πολύπλοκη και χρονοβόρα, και αποτελεί έτσι μία κύρια πρόκληση.
Στην ομιλία αυτή, θα παρουσιάσω την VeriML, μία γλώσσα προγραμματισμού που λειτουργεί ως ένας καινούριος proof assistant, την οποία ανέπτυξα κατά τη διδακτορική μου έρευνα. Ο σχεδιασμός της VeriML ξεκινάει από δύο βασικές παρατηρήσεις.
Πρώτον, για την κατασκευή μεγάλων αποδείξεων, η υλοποίηση ειδικευμένων διαδικασιών αυτοματοποίησης είναι πολύ σημαντική, ώστε ο υπολογιστής να ανακαλύπτει όσο το δυνατόν περισσότερα μέρη της απόδειξης. Δεύτερον, κατά τον έλεγχο μίας απόδειξης, η διαδικασία συλλογισμού που χρησιμοποιείται για τις τετριμμένες λεπτομέρειες που έχουν παραληφθεί θα πρέπει να μπορεί να εμπλουτίζεται μέσω τέτοιων διαδικασιών αυτοματισμού, χωρίς όμως αυτό να έχει ως αποτέλεσμα να θυσιάζεται η αξιοπιστία των αποδείξεων.
Η VeriML είναι μία επέκταση της υπάρχουσας γλώσσας ML ώστε να υποστηρίζει type-safe προγραμματισμό με λογικές προτάσεις και αποδείξεις. Ο σχεδιασμός αυτός επιτρέπει την ανάκτηση και γενίκευση των χαρακτηριστικών των παραδοσιακών proof assistants.
Θα περιγράψω πώς η VeriML λαμβάνει υπόψη τις παραπάνω παρατηρήσεις ώστε να επιτρέψει τον προγραμματισμό ενός ``οικοδομήματος'' διαδικασιών αυτοματοποίησης αποδείξεων με περιορισμένη προσπάθεια, και την κατασκευή συνοπτικών μαθηματικών αποδείξεων στον υπολογιστή που αναφέρουν μόνο τις απαραίτητες λεπτομέρειες.
Comments