Příručka automatizovaného uvažování - Handbook of Automated Reasoning

The Příručka automatizovaného uvažování (ISBN  0444508139, 2128 stran) je sbírka články průzkumu na poli automatické uvažování. Publikováno v červnu 2001 autorem MIT Stiskněte, upravuje John Alan Robinson a Andrej Voronkov. Svazek 1 popisuje metody pro klasická logika, logika prvního řádu s rovností a další teorie a indukce. Svazek 2 kryty vyšší řád, neklasické a další druhy logiky.

Index

Hlasitost 1

Dějiny
Klasická logika
  1. Leo Bachmair, Harald Ganzinger. Prokazování věty o rozlišení, str. 19–99.
  2. Reiner Hähnle. Tablo a související metody, s. 100–178.
  3. Anatoli Degtyarev, Andrej Voronkov. Inverzní metoda, str. 179–272.
  4. Matthias Baaz, Uwe Egly, Alexander Leitsch. Transformace normálních forem, str. 273–333.
  5. Andreas Nonnengart, Christoph Weidenbach. Computing Small Clause Normal Forms, str. 335–367.
Rovnost a další teorie
  1. Robert Nieuwenhuis, Alberto Rubio. Prokazování věty založené na parametru, str. 371–443.
  2. Franz Baader, Wayne Snyder. Teorie sjednocení, str. 445–532.
  3. Nachum Dershowitz, David Plaisted. Přepisování, str. 535–610.
  4. Anatoli Degtyarev, Andrej Voronkov. Odůvodnění rovnosti v sekvenčních kalkulích, s. 611–706.
  5. Shang-Ching Chou, Xiao-Shang Gao. Automated Reasoning in Geometry, str. 707–749.
  6. Alexander Bockmayr, Volker Weispfenning. Řešení numerických omezení, str. 751–842.
Indukce
  1. Alan Bundy. The Automation of Proof by Mathematical Induction, str. 845–911.
  2. Hubert Comon. Indukční indukce, str. 913–962.

Svazek 2

Logika vyšších řádů a logické rámce
Neklasická logika
  1. Jürgen Dix, Ulrich Furbach, Ilkka Niemelä. Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations, s. 1241–1354.
  2. Matthias Baaz, Christian Fermüller, Gernot Salzer. Automated Deduction for Many-Valued Logics, str. 1355–1402.
  3. Hans-Jürgen Ohlbach, Andreas Nonnengart, Maarten De Rijke, Dov Gabbay. Kódování dvouhodnotových neklasických logik v klasické logice, str. 1403–1486.
  4. Arild Waaler. Spojení v neklasické logice, str. 1487–1578.
Rozhodovatelné třídy a tvorba modelů
  1. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi. Odůvodnění v Expressive Description Logics, str. 1581–1634.
  2. Edmund Clarke, Holger Schlingloff. Kontrola modelu, str. 1635–1790.
  3. Christian Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet. Postupy pro rozhodování o řešení problémů, str. 1791–1849.
Implementace
  1. I.V. Ramakrishnan, R. Seekar, Andrej Voronkov. Indexování termínů, str. 1853–1964.
  2. Christoph Weidenbach. Kombinace superpozice, třídění a rozdělení, str. 1965–2013.
  3. Reinhold Letz, Gernot Stenz. Postupy eliminace modelu a tabla, str. 2015–2114.

externí odkazy