|Computational Logic and Logical Programming |
|Title: ||Computational Logic and Logical Programming |
|Lesson Code: ||321-3552|
|Theory Hours: ||3|
|Lab Hours: ||2|
|Faculty: ||Stamatatos Efstathios|
Propositional Logic: Syntax and semantics, Logical entailment, Truth tables, Proof methods (inference rules, axiom schemas, soundness and completeness). Reolution proof in propositional logic and search strategies. Predicate Logic: Syntax and semantics, Herbrand's method, Proof methods (inference rules, axiom schemas, soundness and completeness). Unification and Resolution proof in predicate logic. PROLOG: Syntax and program structure, inference mechanism, cut and negation, applications.
Understanding of syntax and semantics of propositional logic. Ability to apply semantic methods to prove a clause given a set of premises. Familiarity with formal proof methods. Understanding and application of the resolution method in propositional logic. Understanding of syntax and semantics of predicate logic. Familiarity with the application of the Herbrand method. Ability to apply the algorithm of transforming an expression of predicate logic to conjunctive normal form. Understanding and application of the unification method and the algorithm of finding the most general unifier of two clauses in predicate logic. Understanding of the resolution method in predicate logic. Understanding of the basic strategies to apply the resolution method. Familiarity with the main principles of logic programming. Ability to write programs in PROLOG to solve practical problems.
1. Uwe Schoening, “Logic for Computer Scientists”, Birkhauser, 1989.
2. Enderton, H.A., “Mathematical Introduction to Logic”, (2nd ed), San Diego, Cal: Academic Press 2001.
3. Ulf Nilsson and Jan Maluszynski, “Logic, Programming and Prolog” (2nd ed).
4. Michael Spivey, “An introduction to logic programming through Prolog”.
1. Artificial Intelligence (Elsevier)
2. Journal of Artificial Intelligence Research
3. ACM Transactions on Computational Logic
4. Journal of Logic and Computation (OUP)
|Learning Activities and Teaching Methods |
During the teaching hours of the course, teaching material is projected to highlight the characteristics of the examined methods and systems. Appropriate methods and algorithms are demonstrated. The active participation of students with critical questions and small-group discussions is strongly encouraged. Exercises are solved.
|Assessment/Grading Methods |
Ατομικές και ομαδικές εργασίες, πρακτική εξάσκηση στο εργαστήριο, μικρά τεστ στη μορφή κουίζ, τελική γραπτή εξέταση.
||Φόρτος Εργασίας Εξαμήνου
||125 ώρες (5 ECTS)
|Language of Instruction|
|Greek, English (for Erasmus students)|
|Μode of delivery |