El Manual de razonamiento automatizado ( ISBN 0444508139 , 2128 páginas) es una colección de artículos de encuestas sobre el campo del razonamiento automatizado . Publicado en junio de 2001 por MIT Press , está editado por John Alan Robinson y Andrei Voronkov . El volumen 1 describe métodos de lógica clásica , lógica de primer orden con igualdad y otras teorías e inducción . El volumen 2 cubre la lógica de orden superior , no clásica y de otro tipo.
Índice
Volúmen 1
- Historia
- Martin Davis . La historia temprana de la deducción automatizada , págs. 3-15.
- Lógica clásica
- Leo Bachmair , Harald Ganzinger . Demostración del teorema de resolución, págs. 19–99.
- Reiner Hähnle . Cuadros y métodos relacionados, págs. 100-178.
- Anatoli Degtyarev , Andrei Voronkov . El método inverso, págs. 179–272.
- Matthias Baaz , Uwe Egly , Alexander Leitsch . Transformaciones de formas normales, págs. 273–333.
- Andreas Nonnengart , Christoph Weidenbach . Cálculo de formas normales de cláusula pequeña, págs. 335–367.
- Igualdad y otras teorías
- Robert Nieuwenhuis , Alberto Rubio. Demostración de teoremas basada en paramodulación, págs. 371–443.
- Franz Baader , Wayne Snyder . Teoría de la unificación , págs. 445–532.
- Nachum Dershowitz , David Plaisted . Reescritura , págs. 535–610.
- Anatoli Degtyarev , Andrei Voronkov . Razonamiento de igualdad en cálculos basados en secuencia, págs. 611–706.
- Shang-Ching Chou , Xiao-Shang Gao . Razonamiento automatizado en geometría, págs. 707–749.
- Alexander Bockmayr , Volker Weispfenning . Resolver restricciones numéricas, págs. 751–842.
- Inducción
- Alan Bundy . La automatización de la prueba por inducción matemática, págs. 845–911.
- Hubert Comon . Inducción sin inducción, págs. 913–962.
Volumen 2
- Marcos lógicos y lógicos de orden superior
- Peter B. Andrews . Teoría clásica de tipos , págs. 965–1007.
- Gilles Dowek . Unificación y emparejamiento de orden superior , págs. 1009–1062.
- Frank Pfenning . Marcos lógicos , págs. 1063-1147.
- Henk Barendregt , Herman Geuvers . Ayudantes de pruebas que utilizan sistemas de tipos dependientes , págs. 1149-1238.
- Lógicas no clásicas
- Jürgen Dix , Ulrich Furbach , Ilkka Niemelä . Razonamiento no monotónico: hacia cálculos e implementaciones eficientes, págs. 1241-1354.
- Matthias Baaz , Christian Fermüller , Gernot Salzer . Deducción automatizada para lógicas de muchos valores, págs. 1355–1402.
- Hans-Jürgen Ohlbach , Andreas Nonnengart , Maarten De Rijke , Dov Gabbay . Codificación de lógicas no clásicas de dos valores en lógica clásica, págs. 1403–1486.
- Arild Waaler . Conexiones en lógicas no clásicas, págs. 1487-1578.
- Clases decidibles y construcción de modelos
- Diego Calvanese , Giuseppe De Giacomo , Maurizio Lenzerini , Daniele Nardi . Razonamiento en lógica descriptiva expresiva, págs. 1581-1634.
- Edmund Clarke , Holger Schlingloff . Model Checking, págs. 1635–1790.
- Christian Fermüller , Alexander Leitsch , Ullrich Hustadt , Tanel Tammet . Procedimientos de decisión de resolución, págs. 1791–1849.
- Implementación
- IV Ramakrishnan , R.Sekar , Andrei Voronkov . Term Indexing, págs. 1853–1964.
- Christoph Weidenbach . Combinando superposición, ordenación y división, págs. 1965-2013.
- Reinhold Letz , Gernot Stenz . Procedimientos de Tableau de conexión y eliminación de modelos, págs. 2015–2114.