ΘΠ13 Υπολογιστική Λογική

• Κ09 - Διακριτά Μαθηματικά

Εισαγωγή στη λογική. Προτασιακός λογισμός (σύνταξη, σημασιολογία, αποδεικτικά συστήματα Hilbert και Tableaux, εγκυρότητα και πληρότητα). Κατηγορηματικός λογισμός (σύνταξη, σημασιολογία, αποδεικτικά συστήματα Hilbert και Tableaux, εγκυρότητα, θεώρημα πληρότητας του κατηγορηματικού λογισμού). Στοιχεία θεωρίας μοντέλων. Θεώρημα μη-πληρότητας (διατύπωση - συνέπειες). Εφαρμογές της λογικής στην Πληροφορική: θεωρία πεπερασμένων μοντέλων και περιγραφική πολυπλοκότητα (χρήση της λογικής για τον χαρακτηρισμό κλάσεων πολυπλοκότητας, θεώρημα του Fagin). Χρήση μη-κλασικής λογικής για τυπική πιστοποίηση (formal verification) συστημάτων λογισμικού.