Απόδειξη θεωρημάτων. Πρωτοβάθμιος κατηγορηματικός λογισμός, μοντέλα, μοντέλα
Herbrand, clauses, κανονική μορφή, prenex, κανονική μορφή Skolen, resolution,
ορθότητα και πληρότητα του resolution του Robinson. Θεωρία Λογικού
προγραμματισμού, Horn clauses, μέθοδοι έρευνας, η άρνηση ως αποτυχία και η
σημασιολογίατης, μη-μονότονη συλλογιστική, μοντέλα τριών τιμών αλήθειας.
Συναρτησιακός προγραμματισμός: χωρίς τύπους, με τύπους, οι αποδείξεις ως
προγράμματα, ισομορφισμός του Curry-Howard, δευτεροβάθμια λογικά συστήματα,
συστήματα πολυμορφισμού. Σημασιολογία: προγραμματιστικών γλωσσών, θεωρία του
σταθερού σημείου.
- Διδάσκων: Πέτρος Στεφανέας
Διδακτικές Μονάδες : 5
Γλώσσα : el