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)

Description

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.