Files in this item

FilesDescriptionFormat

application/pdf

application/pdf9543540.pdf (4MB)Restricted to U of Illinois
(no description provided)PDF

Description

Title:Using term ordering to control clausal deduction
Author(s):Bronsard, Francois
Doctoral Committee Chair(s):Reddy, Uday S.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(s):Computer Science
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.
Issue Date:1995
Type:Text
Language:English
URI:http://hdl.handle.net/2142/21185
Rights Information:Copyright 1995 Bronsard, Francois
Date Available in IDEALS:2011-05-07
Identifier in Online Catalog:AAI9543540
OCLC Identifier:(UMI)AAI9543540


This item appears in the following Collection(s)

Item Statistics