Αλγεβρικές προδιαγραφές δομών δεδομένων. Εξισωτική λογική: εγκυρότητα και συνεπαγωγή εξισώσεων, το σύστημα των εξισωτικών κανόνων. Συστήματα αναγραφής. Τερματισμός, ιδιότητα Church-Rosser, κανονικές μορφές. Η μέθοδος πεπερασμένων υπο-όρων. Ελάχιστο μοντέλο εξισώσεων. Μη-αποδείξιμες εξισώσεις. Προτάσεις μη-εκφράσιμες μέσω εξισώσεων. Θεώρημα πληρότητας των εξισωτικών κανόνων. Προτασιακοί τύποι. Το σύστημα Gentzen και η έρευνα top-down. Διάψευση προτασιακών τύπων με τη μέθοδο της επίλυσης. Θεωρήματα πληρότητας για το σύστημα Gentzen και για την επίλυση. Τύποι πρώτης τάξης. Το γενικό σύστημα Gentzen και η γενική έρευνα top-down. Θεωρήματα πληρότητας και συμπάγειας. Προτάσεις μη-εκφράσιμες μέσω τύπων πρώτης τάξης. Εισαγωγή στον λογικό προγραμματισμό. Ενοποίηση όρων. Επίλυση καθολικών τύπων. Εισαγωγή στις συμβολικές επαγωγικές αποδείξεις. Κρίσιμα ζεύγη συστημάτων αναγραφής. Η μέθοδος Knuth-Bendix.
