mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Seminars » 2012-2013 » Α. Σταμπούλης, 2013-02-08 { prev, contents, next }
download seminar details: { pdf }

Seminar

Speaker: Αντώνιος Σταμπούλης (Μεταδιδακτορικός Ερευνητής, Massachusetts Institute of Technology)
Title: VeriML: A dependently-typed, user-extensible and language-centric approach to proof assistants
Date: Παρασκευή, 08 Φεβ 2013
Ώρα: 18:30-19:30
Location: Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών, Τμήμα Μαθηματικών, room Γ33

Abstract

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

Comments

You must be logged in to comment.

Reporter

Web standards: XHTML1.0, CSS3.
© 1996 – 2018 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.