Hispanopedia Wiki
Articulo de referencia

Manual de razonamiento automatizado

El manual de razonamiento automatizado ( ISBN) 0444508139 (2128 páginas) es una colección de artículos de revisión sobre el campo del razonamiento automatizado . [ 1 ] Publica...

Hispanopedia WikiContenido en espanolLectura gratuita

El manual de razonamiento automatizado ( ISBN) 0444508139(2128 páginas) es una colección de artículos de revisión sobre el campo del razonamiento automatizado . [ 1 ] Publicado en junio de 2001 por MIT Press , está editado por John Alan Robinson y Andrei Voronkov . El volumen 1 describe métodos para la lógica clásica , la lógica de primer orden con igualdad y otras teorías, y la inducción . El volumen 2 cubre la lógica de orden superior , la lógica no clásica y otros tipos de lógica.

Índice

Volumen 1

Historia
  1. Martin Davis . Los inicios de la deducción automatizada , págs.  3-15.
Lógica clásica
  1. Leo Bachmair , Harald Ganzinger . Demostración de teoremas de resolución, págs.  19-99.
  2. Reiner Hähnle . Cuadros y métodos relacionados, págs.  100–178.
  3. Anatoli Degtyarev , Andrei Voronkov . El método inverso, págs.  179–272.
  4. Matthias Baaz , Uwe Egly , Alexander Leitsch . Transformaciones de forma normal, págs.  273–333.
  5. Andreas Nonnengart , Christoph Weidenbach . Calcular formas normales de cláusulas pequeñas, págs  .
Igualdad y otras teorías
  1. Robert Nieuwenhuis , Alberto Rubio. Demostración de teoremas basada en paramodulación, págs.  371–443.
  2. Franz Baader , Wayne Snyder . Teoría de la unificación , págs.  445–532.
  3. Nachum Dershowitz , David Plaisted . Reescritura , págs.  535–610.
  4. Anatoli Degtyarev , Andrei Voronkov . Razonamiento de igualdad en cálculos basados ​​en secuencias, págs  .
  5. Shang-Ching Chou , Xiao-Shang Gao . Razonamiento automatizado en geometría, págs.  707–749.
  6. Alexander Bockmayr , Volker Weispfenning . Resolución de restricciones numéricas, págs.  751–842.
Inducción
  1. Alan Bundy . La automatización de la demostración por inducción matemática, págs.  845–911.
  2. Hubert Comon . Inducción sin inducción, págs.  913–962.

Volumen 2

Lógica de orden superior y marcos lógicos
  1. Peter B. Andrews . Teoría clásica de tipos , págs.  965–1007.
  2. Gilles Dowek . Unificación y emparejamiento de orden superior , págs.  1009–1062.
  3. Frank Pfenning . Marcos lógicos , págs.  1063–1147.
  4. Henk Barendregt , Herman Geuvers . Asistentes de prueba que utilizan sistemas de tipos dependientes , págs  .
Lógicas no clásicas
  1. Jürgen Dix , Ulrich Furbach , Ilkka Niemelä . Razonamiento no monótono: hacia cálculos e implementaciones eficientes, págs.  1241–1354.
  2. Matthias Baaz , Christian Fermüller , Gernot Salzer . Deducción automatizada para lógicas multivaluadas, págs.  1355–1402.
  3. 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  .
  4. Arild Waaler . Conexiones en lógicas no clásicas, págs.  1487–1578.
Clases decidibles y construcción de modelos
  1. Diego Calvanese , Giuseppe De Giacomo , Maurizio Lenzerini , Daniele Nardi . Razonamiento en lógicas de descripción expresiva, págs.  1581-1634.
  2. Edmund Clarke , Holger Schlingloff . Comprobación de modelos, págs.  1635-1790.
  3. Christian Fermüller , Alexander Leitsch , Ullrich Hustadt , Tanel Tammet . Procedimientos de decisión de resolución, págs.  1791–1849.
Implementación
  1. IV Ramakrishnan , R.Sekar , Andrei Voronkov . Indexación de términos, págs.  1853-1964.
  2. Christoph Weidenbach . Combinando superposición, tipos y división, págs.  1965–2013.
  3. Reinhold Letz , Gernot Stenz . Procedimientos de Tableau para la eliminación y conexión de modelos, págs.  2015–2114.

Referencias

  1. ↑ Russell, Stuart Jonathan; Norvig, Peter; Davis, Ernest (2009). Inteligencia artificial: un enfoque moderno . Prentice Hall . pág. 360. ISBN  9780136042594. Consultado el 1 de diciembre de 2025 .
  • Página de prensa del MIT