Ivo Robert

1. first-order logic
2. theorem proving
3. automatic proving systems

Upon completion of this learning unit (LU), the student should be able to:
- identify the underlying theories to automatic theorem proving.
- apply automatic deduction to different mathematical problems, such as minimization of theories, determination of counter-examples, theorem proving.

This course unit studies in depth the theory of logic programming, aiming at  analysing processes of automatic proving of theorems. Some of the topics covered are: formulas and interpretations in logic, normal forms, Herbrand's theorem, principle of resolution, semantic resolution, linear resolution, paramodulation.

C. L. Chang, R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, London, 1973.
J. A. Kalman: Automated Reasoning with OTTER, Rinton Press, Princeton, New Jersey, 2001.

E-learning (fully online).

Evaluation is made on individual basis and it involves the coexistence of two modes: continuous assessment (60%) and final evaluation (40%). Further information is detailed in the Learning Agreement of the course unit.