Symposium on Automatic Demonstration

Inhaltsverzeichnis

• 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.