{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/21185"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/21185","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Using term ordering to control clausal deduction","abstract":"ETDs are only available to UIUC Users without author permission","abstract_html":"ETDs are only available to UIUC Users without author permission","abstract_has_math":false,"creators":["Bronsard, Francois"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Reddy, Uday S."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T13:00:56Z","date_published":"2011-05-07T13:00:56Z","updated_at":"2026-07-22T22:25:17Z","subjects":["Computer Science"],"languages":["eng"],"rights":["Copyright 1995 Bronsard, Francois"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9543540","(UMI)AAI9543540"],"render_values":[{"text":"AAI9543540","href":null,"code":true},{"text":"(UMI)AAI9543540","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/21185","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Reddy, Uday S."]},{"key":"dc:creator","label":"Author","values":["Bronsard, Francois"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T13:00:56Z","10000-01-01","1995"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 1995 Bronsard, Francois"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9543540","(UMI)AAI9543540","http://hdl.handle.net/2142/21185"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["ETDs are only available to UIUC Users without author permission","U of I Only","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.","Made available in DSpace on 2011-05-07T13:00:56Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9543540.pdf: 4160408 bytes, checksum: 19e97dac9fa62bc5fc4aefe135f765ca (MD5) Previous issue date: 1995","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:49:03Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:16-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission"]},{"key":"dc:title","label":"Title","values":["Using term ordering to control clausal deduction"]}]}],"canonical_facts":{"dc:contributor":["Reddy, Uday S."],"dc:creator":["Bronsard, Francois"],"dc:date":["2011-05-07T13:00:56Z","10000-01-01","1995"],"dc:description":["ETDs are only available to UIUC Users without author permission","U of I Only","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.","Made available in DSpace on 2011-05-07T13:00:56Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9543540.pdf: 4160408 bytes, checksum: 19e97dac9fa62bc5fc4aefe135f765ca (MD5) Previous issue date: 1995","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:49:03Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:16-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission"],"dc:identifier":["AAI9543540","(UMI)AAI9543540","http://hdl.handle.net/2142/21185"],"dc:language":["eng"],"dc:rights":["Copyright 1995 Bronsard, Francois"],"dc:subject":["Computer Science"],"dc:title":["Using term ordering to control clausal deduction"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:17Z"}