Εφαρμοσμένη Θεωρία Αποδείξεων
Χειμερινό εξάμηνο 2013–14
Τρίτη 16:15–18:00 και Παρασκευή 11:00–12:45, αίθουσα 101/102 (ανάλογα με τη διαθεσιμότητα), νέα κτήρια ηλεκτρολόγων ΕΜΠ.Περίληψη
Το μάθημα αυτό αποτελεί μία εισαγωγή στις βασικές έννοιες και μεθόδους τής ερμηνευτικής θεωρίας αποδείξεων και στην χρήση τους στην απόπλεξη αποδείξεων (unwinding of proofs), ήτοι στην εξαγωγή κατασκευαστικής πληροφορίας από (ενδεχομένως μη κατασκευαστικές) μαθηματικές αποδέιξεις. Η απόπλεξη αποδείξεων, η οποία έχει την αφετηρία της στη δουλειά τού G. Kreisel κατά τη δεκαετία τού '50, έχει εφαρμογές τόσο στα μαθηματικά, όπως ο υπολογισμός άνω φραγμάτων και η εκτίμηση της λογικής πολυπλοκότητας αποδείξεων, όσο και στην θεωρία τού υπολογισμού, όπως η σύνθεση αριθμητικών αλγορίθμων και ο προγραμματισμός με αποδείξεις.
Περιεχόμενα
- Εισαγωγή στην απόπλεξη αποδείξεων
- Αριθμητική σε όλους τούς πεπερασμένους τύπους
- Πολωνικοί χώροι
- Τροποποιημένη πραγματοποιησιμότητα
- Συναρτησιακή ερμηνεία
- Εφαρμογές στην ανάλυση
Σημειώσεις παραδόσεων
2014.3.24 (pdf, αγγλικά)Παλαιότερες: 2014.3.2 (pdf, αγγλικά), 2014.2.12 (pdf, αγγλικά)
Θέματα εξετάσεων
Exam.pdfΒιβλιογραφία
- U. Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer-Verlag, 2008.