E-Book, Englisch, Band 125, 310 Seiten, eBook
Reihe: Lecture Notes in Mathematics
Laudet / Lacombe / Nolin Symposium on Automatic Demonstration
Erscheinungsjahr 2006
ISBN: 978-3-540-36262-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Held at Versailles/France, Decembre 1968
E-Book, Englisch, Band 125, 310 Seiten, eBook
Reihe: Lecture Notes in Mathematics
ISBN: 978-3-540-36262-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
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.