6th Conference on Automated Deduction

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.