Symposium on Automatic Demonstration

Held at Versailles/France, Decembre 1968
Herausgegeben:Laudet, M.; Lacombe, D.; Nolin, L.; Schützenberger, M.

• Broschiertes Buch

Produktbeschreibung

Allocution d'ouverture.- Presentation d'un langage de formalisation des demonstrations mathematiques naturelles.- The mathematical language AUTOMATH, its usage, and some of its extensions.- Proof theory and the accuracy of computations.- Aspects du Theoreme de completude selon Herbrand.- Decision procedure for theories categorical in Alefo.- On the long-range prospects of automatic theorem-proving.- The case for using equality axioms in automatic demonstration.- Hilbert's programme and the search for automatic proof procedures.- A linear format for resolution.- Refinement theorems in resolution theory.- Definitional approach to automatic demonstration.- Heuristic interest of using metatheorems.- A proof procedure with matrix reduction.- Axiom systems in automatic theorem proving.- Constructive validity.- Paramodulation and set of support.

Produktdetails

• Lecture Notes in Mathematics 125
• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 978-3-540-04914-2
• 1970.
• Seitenzahl: 320
• Erscheinungstermin: 1. Januar 1970
• Englisch
• Abmessung: 235mm x 155mm x 18mm
• Gewicht: 508g
• ISBN-13: 9783540049142
• ISBN-10: 3540049142
• Artikelnr.: 23380387

Inhaltsangabe

Allocution d'ouverture.- Presentation d'un langage de formalisation des demonstrations mathematiques naturelles.- The mathematical language AUTOMATH, its usage, and some of its extensions.- Proof theory and the accuracy of computations.- Aspects du Theoreme de completude selon Herbrand.- Decision procedure for theories categorical in Alefo.- On the long-range prospects of automatic theorem-proving.- The case for using equality axioms in automatic demonstration.- Hilbert's programme and the search for automatic proof procedures.- A linear format for resolution.- Refinement theorems in resolution theory.- Definitional approach to automatic demonstration.- Heuristic interest of using metatheorems.- A proof procedure with matrix reduction.- Axiom systems in automatic theorem proving.- Constructive validity.- Paramodulation and set of support.