A structured design-method for specialized proof procedures

• Main Author: Brown, Thomas Carl
• Format: Others
• Language: en
• Published: 1975
• Online Access: https://thesis.library.caltech.edu/6541/4/Brown_t_1975.pdf; Brown, Thomas Carl (1975) A structured design-method for specialized proof procedures. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/nrh8-ka82. https://resolver.caltech.edu/CaltechTHESIS:07182011-144905895 <https://resolver.caltech.edu/CaltechTHESIS:07182011-144905895>

A proof procedure verifies relative consequence relations B ⊨_E C (1) in first-order logic with equality by generating a refutation (or proof of contradiction) for some clause-representation C of B ˘ {¬ C}, using the axioms and inferences of some sound and effective calculus for ⊨_E. Performance of the procedure depends upon two forms of heuristic knowledge about ⊨_E. which it may embody: (S) Structural knowledge is formalized by a refinement (or decidable subset) of the deductions admitted by the procedure's calculus which acts as a "search-space filter": only those deductions from C contained in the refinement are generated. (P) Procedural knowledge is formalized by a search strategy (or enqueing function): it determines which of the admissible inferences will be generated next on the basis of the current deduction. This investigation develops a general hierarchical method for the design of refinements embodying structural forms of heuristic knowledge characteristic of expert human problem solvers in an axiomatized problem domain. Initially we design refinement Δ for E-resolution deductions, whose inferences have the form {B_1 v q_1,...,B_n v q_n} ⊢ C (2) where (b_1 -q_1) θ v ... v (B_n - q_n) θ ≥ C ≥ (B_1 θ - q_1θ) v...v (B_nθ-q_nθ) and θ is a substitution (of terms for variables) which makes {q_1θ,...q_nθ} contradictory in E. The unit-clause set {q_1,...,q_n} is called a latent E-contradiction. E-resolution is not in general effective: each inference (2) must be realized by finding a "lower level" refutation for E ˘ {q_1,...,q_n} and extracting θ from it. For this sub-problem we design and E'-resolution refinement Δ' where E > E'. The normal composition Δ • Δ' consists of deductions in Δ wherein each inference (2) is "realized" by a refutation in Δ'; Δ • Δ' is actually an E'-resolution refinement. Iterating the above (with E' for E), we obtain an E_o-resolution refinement Δ_M = (...(Δ_n • Δ_(n-1))...Δ_o) where Δ_k is an E_k-resolution refinement and E = E_n >...>E_o = unit clauses of E. An E_o-resolution inference is realized by refuting a latent A-contradiction {p,q} where A is a set of equations including E_o˘{[x=x]}. For this sub-problem we design an (E_o-) resolution micro-refinement Δ_µ for the set of deductions composed of factoring, binary resolution, and paramodulation inferences. Normal refinements Δ_M • Δ_µ combine the composite structural knowledge embodied in Δ_M with the effectiveness, efficiency, and most-general inference properties of Δ_µ. Hyper-E-resolution (HR(E,≻,s)) exemplifies Δ_µ. ≻ is an "invariant complexity ordering" which well-orders constant terms. For each resolution inference {A v p, B v Q} ⊢ (A v B)θ in a member of ND(E,≻), underlined literals must have been reduced to a "least complex" normal form by a chain of ≻ -ordered replacement operations based on equations of E and current derived equations; moreover, tθ cannot be "more complex" than sθ. "Functional reflexivity" equations [fx_1...x_n = fx_1...x_n], being sudsumed by [x=x], are excluded from E-normal deductions by strong subsumption-deletion constraints. Theorem B. ND (E,≻) is refutation complete on unit-clause sets. Corollary. If E and Δ_M are as in Theorem A and no non-unit clause of E contains a (positive) equation then Δ_M • ND(E_o,≻) is refutation complete on clause-sets whose non-unit clauses each contain at most one equation. Normal refinements are illustrated in the solutions of several refutation problems in Group Theory and Integer Arithmetic, where useful forms and complexity orderings are employed.