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