First-order predicate calculus, models, Herbrand models, clauses, normal forms, prenex, Skolem normal form, resolution.
Correctness and completeness of Robinson resolution.
Theory of Logical Programming: Horn clauses, negation as failure and its semantics, non-monotonic reasoning, 3-valued models.
Functional programming: untyped, typed, proofs as programs, Curry-Howard isomorphism.
Second-order logical systems, polymorphism.
Semantics: programming languages, fixed point.
Algebraic specifications.
Introduction to category theory.
- Teacher: Πέτρος Στεφανέας
ECTS : 5
Language : el