Τμήμα : Γενικό
Τομέας : Μαθηματικών
Κωδικός : Νέο
Εξάμηνο : 8ο
Ροή : Μ : Μαθηματικά
Κατ' επιλογήν υποχρεωτικό.
Ώρες Θεωρίας : 3
Ώρες Εργαστηρίου : 1
Περιεχόμενο του μαθήματος :
Απόδειξη θεωρημάτων. Πρωτοβάθμιος κατηγορηματικός λογισμός, Μοντέλα, Μοντέλα Herbrand, clauses, Κανονική μορφή, prenex, Κανονική μορφή Skolen, Resolution, Ορθότητα και πληρότητα του resolution του Robinson. Θεωρία Λογικού προγραμματισμού, Horn clauses, Μέθοδοι έρευνας, η άρνηση ως αποτυχία και η σημασιολογία της, μη-μονότονη συλλογιστική, μοντέλα τριών τιμών αλήθειας. Συναρτησιακός προγραμματισμός, χωρίς τύπους, με τύπους οι αποδείξεις ως προγράμματα, ισομορφισμός του Curry-Howard, Δευτεροβάθμια λογικά συστήματα, συστήματα πολυφορμισμού. Σημασιολογία προγραμματιστικών γλωσσών, θεωρία του σταθερού σημείου.