Applications of Logic in Computer Science

Code 9.2.3317.8
Semester 8th
Flow M - Mathematics
Category Obligatory by selection
Credits 4
Class Hours - Lab Hours 4 - 0
Lecturers Giorgos Koletsos, Petros Potikas (T & R Associates), Petros Stefaneas (School of AMPS)


Theorem proving. First-order predicate calculus, models, Herbrand models, canonical forms, prenex, Skolem normal forms, resolution, soundness and completeness of Robinson's resolution principle. Theory of logic programming, Horn clauses, search methods, negation as failure and its semantics, non-monotonic reasoning and three-valued logics. Functional programming with and without types, proofs as programs, the Curry-Howard isomorphism, second-order logic and polymorphic systems. Semantics of programming languages and fixpoint theory.