Demostración automática de teoremas (2002-03)
Este curso es una introducción a la demostración automática usando Otter y Mace2.
Temas
Bibliografía
- J.A. Alonso, A. Fernández y M.J. Pérez. Razonamiento automático (Univ. Sevilla, 1996).
- A. Bundy. The computer modelling of mathematical reasoning. (Academic Press, 1983).
- C.L. Chang y R.C.T. Lee. Symbolic logic and mechanical theorem proving. (Academic Press, 1973).
- M. Davis. The early history of automated deduction.
- M.R. Genesereth y N.J. Nilsson. Logical foundations of artificial intelligence. (Morgan Kaufmann, 1987).
- G. Kolata. Computer math proof shows reasoning power (The New York Times, 10 de diciembre de 1996).
- W. McCune. Otter 3.3 reference manual.
- N.J. Nilsson. Artificial intelligence: A new synthesis. (McGraw–Hill, 1998).
- G. Sutcliffe. What is automated theorem proving?
- L. Wos, R. Overbeek, E. Lusk. y J. Boyle. Automated reasoning: Introduction and applications. (McGraw–Hill, 1992).