Εφαρμογές της Λογικής στην Πληροφορική
| Code | 9.2.3317.8 |
|---|---|
| Semester | 8th |
| Category | |
| Credits | 4 |
| Class Hours - Lab Hours | 4 - 0 |
| Lecturers | Giorgos Koletsos, Petros Potikas, Petros Stefaneas |
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.