Format:
Online-Ressource (VII, 389 S.)
Edition:
Online-Ausg. Berlin [u.a.] Springer 2006 Springer lecture notes archive
ISBN:
9783540392408
Series Statement:
Lecture notes in computer science 138
Content:
Solving open questions with an automated theorem-proving program -- STP: A mechanized logic for specification and verification -- A look at TPS -- Logic machine architecture: Kernel functions -- Logic machine architecture: Inference mechanisms -- Procedure implementation through demodulation and related tricks -- The application of Homogenization to simultaneous equations -- Meta-level inference and program verification -- An example of FOL using metatheory -- Comparison of natural deduction and locking resolution implementations -- Derived preconditions and their use in program synthesis -- Automatic construction of special purpose programs -- Deciding combinations of theories -- Exponential improvement of efficient backtracking -- Exponential improvement of exhaustive backtracking: data structure and implementation -- Intuitionistic basis for non-monotonic logic -- Knowledge retrieval as limited inference -- On indefinite databases and the closed world assumption -- Proof by matrix reduction as plan + validation -- Improvements of a tautology-testing algorithm -- Representing infinite sequences of resolvents in recursive First-Order Horn Databases -- The power of the Church-Rosser property for string rewriting systems -- Universal unification and a classification of equational theories.
Note:
Literaturangaben
Additional Edition:
ISBN 3540115587
Additional Edition:
ISBN 0387115587
Additional Edition:
ISBN 9783540115588
Additional Edition:
Erscheint auch als Druck-Ausgabe Conference on Automated Deduction (6 : 1982 : New York, NY) 6th Conference on Automated Deduction Berlin [u.a.] : Springer, 1982 ISBN 3540115587
Additional Edition:
ISBN 0387115587
Language:
English
Keywords:
Konferenzschrift
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
