Hugendubel.info - Die B2B Online-Buchhandlung 

Merkliste
Die Merkliste ist leer.
Bitte warten - die Druckansicht der Seite wird vorbereitet.
Der Druckdialog öffnet sich, sobald die Seite vollständig geladen wurde.
Sollte die Druckvorschau unvollständig sein, bitte schliessen und "Erneut drucken" wählen.

Automation of Reasoning

2: Classical Papers on Computational Logic 1967-1970
BuchKartoniert, Paperback
637 Seiten
Englisch
Springererschienen am09.02.2012Softcover reprint of the original 1st ed. 1983
The article by Martin Davis in the first of this series of volumes traces the most influential ideas back to the 'prehistory' of early logical thought showing how these ideas influenced the underlying concepts of most early automatic theorem proving programs.mehr

Produkt

KlappentextThe article by Martin Davis in the first of this series of volumes traces the most influential ideas back to the 'prehistory' of early logical thought showing how these ideas influenced the underlying concepts of most early automatic theorem proving programs.
Details
ISBN/GTIN978-3-642-81957-5
ProduktartBuch
EinbandartKartoniert, Paperback
Verlag
Erscheinungsjahr2012
Erscheinungsdatum09.02.2012
AuflageSoftcover reprint of the original 1st ed. 1983
ReiheArtificial Intelligence
Seiten637 Seiten
SpracheEnglisch
Gewicht1124 g
IllustrationenXII, 637 p.
Artikel-Nr.18233382

Inhalt/Kritik

Inhaltsverzeichnis
Automated Theorem Proving 1965-1970.- 1967.- A Cancellation Algorithm for Elementary Logic.- An Inverse Method for Establishing Deducibility of Nonprenex Formulas of the Predicate Calculus.- Automatic Theorem Proving With Renamable and Semantic Resolution.- The Concept of Demodulation in Theorem Proving.- 1968.- Resolution with Merging.- On Simplifying the Matrix of a WFF.- Mechanical Theorem-Proving by Model Elimination.- The Generalized Resolution Principle.- New Directions in Mechanical Theorem Proving.- Automath, a Language for Mathematics.- 1969.- Semi-Automated Mathematics.- Semantic Trees in Automatic Theorem-Proving.- A Simplified Format for the Model Elimination Theorem-Proving Procedure.- Theorem-Provers Combining Model Elimination and Resolution.- Relationship between Tactics of the Inverse Method and the Resolution Method.- E-Resolution: Extension of Resolution to Include the Equality Relation.- 1969.- Advances and Problems in Mechanical Proof Procedures.- Paramodulation and Theorem-Proving in First-Order Theories with Equality.- 1970.- Completeness Results for E-Resolution.- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness.- The Unit Proof and the Input Proof in Theorem Proving.- Simple Word Problems in Universal Algebras.- The Case for Using Equality Axioms in Automatic Demonstration.- A Linear Format for Resolution.- An Interactive Theorem-Proving Program.- Refinement Theorems in Resolution Theory.- On the Complexity of Derivation in Propositional Calculus.- After 1970.- Resolution in Type Theory.- Splitting and Reduction Heuristics in Automatic Theorem Proving.- A Computer Algorithm for the Determination of Deducibility on the Basis of the Inverse Method.- Linear Resolution with Selection Function.- MaximalModels and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving.- Bibliography on Computational Logic.mehr