Citation
Brown, Thomas Carl (1975) A structured designmethod for specialized proof procedures. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/nrh8ka82. https://resolver.caltech.edu/CaltechTHESIS:07182011144905895
Abstract
A proof procedure verifies relative consequence relations B ⊨_E C (1) in firstorder logic with equality by generating a refutation (or proof of contradiction) for some clauserepresentation 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 "searchspace 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 Eresolution 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 unitclause set {q_1,...,q_n} is called a latent Econtradiction. Eresolution 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 subproblem 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_oresolution refinement Δ_M = (...(Δ_n • Δ_(n1))...Δ_o) where Δ_k is an E_kresolution refinement and E = E_n >...>E_o = unit clauses of E. An E_oresolution inference is realized by refuting a latent Acontradiction {p,q} where A is a set of equations including E_o˘{[x=x]}. For this subproblem we design an (E_o) resolution microrefinement Δ_µ 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 mostgeneral inference properties of Δ_µ. HyperEresolution (HR(E,≻,s)) exemplifies Δ_µ. ≻ is an "invariant complexity ordering" which wellorders 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 Enormal deductions by strong subsumptiondeletion constraints. Theorem B. ND (E,≻) is refutation complete on unitclause sets. Corollary. If E and Δ_M are as in Theorem A and no nonunit clause of E contains a (positive) equation then Δ_M • ND(E_o,≻) is refutation complete on clausesets whose nonunit 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.
Item Type:  Thesis (Dissertation (Ph.D.))  

Subject Keywords:  Computer Science  
Degree Grantor:  California Institute of Technology  
Division:  Engineering and Applied Science  
Major Option:  Computer Science  
Thesis Availability:  Public (worldwide access)  
Research Advisor(s): 
 
Thesis Committee: 
 
Defense Date:  4 December 1974  
Funders: 
 
Record Number:  CaltechTHESIS:07182011144905895  
Persistent URL:  https://resolver.caltech.edu/CaltechTHESIS:07182011144905895  
DOI:  10.7907/nrh8ka82  
Default Usage Policy:  No commercial reproduction, distribution, display or performance rights in this work are provided.  
ID Code:  6541  
Collection:  CaltechTHESIS  
Deposited By:  Benjamin Perez  
Deposited On:  19 Jul 2011 15:25  
Last Modified:  16 Apr 2021 23:32 
Thesis Files

PDF
 Final Version
See Usage Policy. 47MB 
Repository Staff Only: item control page