Λογική και Λογικός Προγραμματισμός

Εκτύπωση

Στόχος

Στόχος του μαθήματος είναι η εισαγωγή στο συντακτικό και στη σημασιολογία του προτασιακού και του κατηγορηματικού λογισμού, η κατανόηση και χρήση των συστημάτων αποδείξεων (συστήματα φυσικής συμπερασματολογίας (natural deduction)), του προτασιακού και κατηγορηματικού λογισμού και τέλος η κατανόηση των θεωρημάτων ορθότητας και πληρότητας των συστημάτων αποδείξεων.

Περιεχόμενα

  • Προτασιακός Λογισμός: Γλώσσα, σύνταξη (syntax) και σημασιολογία (semantics), Μοναδική αναγνωσιμότητα, Λογικοί σύνδεσμοι, απονομές αλήθειας, σημασιολογικές έννοιες, επάρκεια συνδέσμων, διαζευκτική και συζευκτική κανονική μορφή, εφαρμογές.
  • Πρωτοβάθμιος κατηγορηματικός λογισμός: Γλώσσα, μεταβλητές, έννοιες ελεύθερης και δεσμευμένης μεταβλητής, αντικατάσταση, αναλογία με τον προγραμματισμό, η έννοια της δομής, ερμηνεία της γλώσσας, ορισμός της αλήθειας κατά Tarski.
  • Αποδεικτική θεωρία προτασιακού και κατηγορηματικού λογισμού: Αποδεικτικές διαδικασίες Natural Deduction, Tableaux και Επίλυσης (Resolution), ορθότητα (soundness) και πληρότητα (completeness) των διαδικασιών αυτών.
  • Εφαρμογές στην Πληροφορική (διατύπωση και έλεγχος ιδιοτήτων προγραμμάτων).
  • Μητακίδης (1992): Από τη Λογική στο Λογικό Προγραμματισμό και την Prolog, Εκδόσεις Καρδαμίτσα.
  • Σημειώσεις Διδάσκοντα.