Demonstração Automática de Teoremas
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
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.
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.