Author(s): L. Wos (auth.), D. W. Loveland (eds.)
Series: Lecture Notes in Computer Science 138
Edition: 1
Publisher: Springer Berlin Heidelberg
Year: 1982
Language: English
Pages: 399
Tags: Mathematical Logic and Formal Languages
Solving open questions with an automated theorem-proving program....Pages 1-31
STP: A mechanized logic for specification and verification....Pages 32-49
A look at TPS....Pages 50-69
Logic machine architecture: Kernel functions....Pages 70-84
Logic machine architecture: Inference mechanisms....Pages 85-108
Procedure implementation through demodulation and related tricks....Pages 109-131
The application of Homogenization to simultaneous equations....Pages 132-143
Meta-level inference and program verification....Pages 144-150
An example of FOL using metatheory....Pages 151-158
Comparison of natural deduction and locking resolution implementations....Pages 159-171
Derived preconditions and their use in program synthesis....Pages 172-193
Automatic construction of special purpose programs....Pages 194-208
Deciding combinations of theories....Pages 209-222
Exponential improvement of efficient backtracking....Pages 223-239
Exponential improvement of exhaustive backtracking: data structure and implementation....Pages 240-259
Intuitionistic basis for non-monotonic logic....Pages 260-273
Knowledge retrieval as limited inference....Pages 274-291
On indefinite databases and the closed world assumption....Pages 292-308
Proof by matrix reduction as plan + validation....Pages 309-325
Improvements of a tautology-testing algorithm....Pages 326-341
Representing infinite sequences of resolvents in recursive First-Order Horn Databases....Pages 342-359
The power of the Church-Rosser property for string rewriting systems....Pages 360-368
Universal unification and a classification of equational theories....Pages 369-389
