6th Conference on Automated Deduction: New York, USA, June 7–9, 1982

L. Wos (auth.), D. W. Loveland (eds.)3540115587, 9783540115588

6th Conference in Automated DeductionNew York, USA, June 7-9, 1982

---

Table of contents :
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