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.