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