Είσοδος

Λογική και Πληροφορική Ι: Εφαρμογές της Λογικής στον (συναρτησιακό) προγραμματισμό

Γενικά στοιχεία

 

 
Ύλη

Μάθημα: Εφαρμοσμένη Θεωρία Αποδείξεων

Διδάσκοντες:  Γ. Κολέτσος, Ν. Ρήγας

 

http://www.math.ntua.gr/logic/  (Εφαρμοσμένη Θεωρία Αποδείξεων)

 

Το μάθημα αυτό αποτελεί μια εισαγωγή στις βασικές έννοιες και μεθόδους της ερμηνευτικής θεωρίας αποδείξεων και στην χρήση τους στην απόπλεξη αποδείξεων (unwinding of proofs), ήτοι στην εξαγωγή κατασκευαστικής πληροφορίας από (ενδεχομένως μη κατασκευαστικές) μαθηματικές αποδείξεις. Η απόπλεξη αποδείξεων, η οποία έχει την αφετηρία της στη δουλειά τού G. Kreisel κατά τη δεκαετία τού '50, έχει εφαρμογές τόσο στα μαθηματικά, όπως ο υπολογισμός άνω φραγμάτων και η εκτίμηση της λογικής πολυπλοκότητας αποδείξεων, όσο και στην θεωρία τού υπολογισμού, όπως η σύνθεση αριθμητικών αλγορίθμων και ο προγραμματισμός με αποδείξεις.

 

Μέρες-Ώρες.   Τρίτη 4.00-6.00,  αίθουσα 101, Νέα κτήρια Ηλεκτρολόγων, ΕΜΠ

                              Παρασκευή 12.30-14.30, αίθουσα 101, Νέα κτήρια Ηλεκτρολόγων, ΕΜΠ

 

 

Πρώτο μάθημα την Τρίτη 14 Ιανουαρίου 2014



Συγχρηματοδότηση
από την Ε.Ε.