mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Seminars » 2012-2013 » A. Stampoulis, 2013-02-08 { prev, contents, next } Anonymously browsing from 54.159.113.182 at 00:04:32, 22-09-2017. login
download seminar details: { pdf }

Seminar

Speaker: Antonios Stampoulis (Postdoctoral Researcher, Massachusetts Institute of Technology)
Title: VeriML: A dependently-typed, user-extensible and language-centric approach to proof assistants
Date: Friday, 08 Feb 2013
Time: 18:30-19:30
Location: Univeristy of Athens, Department of Mathematics, University of Athens, 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

Page updates

No recent updates.

Feeds RSS and Atom feeds

posts
all posts RSS
news RSS
announcements RSS
website news RSS
events
all events RSS
defenses RSS
exams RSS
seminars RSS
graduations RSS
Web standards: XHTML1.0, CSS3.
© 1996 – 2017 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.