Symposium on Automatic Demonstration
Springer Berlin (Verlag)
978-3-540-04914-2 (ISBN)
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.
| Erscheint lt. Verlag | 1.1.1970 |
|---|---|
| Reihe/Serie | Lecture Notes in Mathematics |
| Zusatzinfo | VI, 310 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 454 g |
| Themenwelt | Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika |
| Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre | |
| Schlagworte | Datenverarbeitung • Mathematica • Proof • Proof theory • Theorem |
| ISBN-10 | 3-540-04914-2 / 3540049142 |
| ISBN-13 | 978-3-540-04914-2 / 9783540049142 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
