Εφαρμογές της Λογικής στην Πληροφορική


Κωδικός 9.2.3317.8
Εξάμηνο 8o
Ροή Μ - Μαθηματικά
Κατηγορία Κατ' επιλογήν υποχρεωτικό
Ώρες Διδασκαλίας - Ώρες Εργαστηρίου 4 - 0
Διδάσκοντες Γεώργιος Κολέτσος, Πέτρος Ποτίκας (Ε.ΔΙ.Π.), Πέτρος Στεφανέας (Σχολή ΕΜΦΕ)

Περιγραφή

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