This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/21185
Description
Title
Using term ordering to control clausal deduction
Author(s)
Bronsard, Francois
Issue Date
1995
Doctoral Committee Chair(s)
Reddy, Uday S.
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
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 an 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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
