Automatic Theorem Proving

Automatic Theorem Proving

Cod: 22014

Department: DCET

Department: DCET

ECTS: 5

Scientific area: Information and Communication Technologies

Scientific area: Information and Communication Technologies

Total working hours: 130

Total contact time: 20

Total contact time: 20

This course unit introduces the mechanical demonstration of theorems using the computer.

- first-order logic
- theorem proving
- automatic proving systems

- 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.

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.