Using Term Ordering to Control Clausal Deduction
Description:... Abstract: "In this thesis we develop the use of term orders as a control paradigm for first-order reasoning. The starting point of our work is Knuth and Bendix's successful completion method for equational reasoning. This method combines a [sic] order-based strategy --saturation by critical inferences -- with a powerful order-based simplification scheme -- simplification by rewriting. Our goal in this work is to develop, and prove correct and complete, a similar method for clausal deduction. First, we develop a technique, called reductive deduction, which is an adaptation of the rewriting inference for clausal reasoning. Similarly, we develop a notion of critical inferences for clausal reasoning inspired by the critical inferences for equational reasoning. Using these techniques we define a clausal completion method that generalizes Knuth and Bendix's equational completion procedure. We show the completeness of our clausal completion method by generalizing the technique used to prove the completeness of the equational completion method. This technique relies on three properties of equivalence relation, the Church-Rosser property, the confluence property, and the local confluence property, and a proof-theoretic method, the proof transformation method. We propose adaptations for clausal deductions of these properties and of that method. The result is a simple and intuitive completeness proof. To apply the proof transformation method, we developed a novel technique of proof representation: clausal proof nets. Clausal proof nets are inspired by Girard's proof nets for Linear Logic. They are graph structures allowing a compact and abstract representation of proofs."
Show description