{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/23046"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/23046","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Proofs and computations in conditional equational theories","abstract":"Conditional equations arise naturally in the algebraic specification of data types. They also provide an elegant computational paradigm that cleanly combines logic and functional programming. In this thesis, we study how to do proofs and computations in conditional equational theories, using rewriting techniques.","abstract_html":"Conditional equations arise naturally in the algebraic specification of data types. They also provide an elegant computational paradigm that cleanly combines logic and functional programming. In this thesis, we study how to do proofs and computations in conditional equational theories, using rewriting techniques.","abstract_has_math":false,"creators":["Sivakumar, G."],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Dershowitz, Nachum"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T14:00:13Z","date_published":"2011-05-07T14:00:13Z","updated_at":"2026-07-22T22:25:21Z","subjects":["Computer Science"],"languages":["eng"],"rights":["Copyright 1989 Sivakumar, G."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI8924945","(UMI)AAI8924945"],"render_values":[{"text":"AAI8924945","href":null,"code":true},{"text":"(UMI)AAI8924945","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/23046","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Dershowitz, Nachum"]},{"key":"dc:creator","label":"Author","values":["Sivakumar, G."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T14:00:13Z","10000-01-01","1989"]},{"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 1989 Sivakumar, G."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI8924945","(UMI)AAI8924945","http://hdl.handle.net/2142/23046"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Conditional equations arise naturally in the algebraic specification of data types. They also provide an elegant computational paradigm that cleanly combines logic and functional programming. In this thesis, we study how to do proofs and computations in conditional equational theories, using rewriting techniques.","\"We examine different formulations of conditional equations as rewrite systems and compare their expressive power. We identify a class of \"\"decreasing\"\" systems for which most of the basic notions (like rewriting and computing normal forms) are decidable. We then study how to determine if a conditional rewrite system is \"\"confluent.\"\" We settle negatively the question whether \"\"joinability of critical pairs\"\" is, in general, sufficient for confluence of terminating conditional systems. We also prove two positive results for systems having critical pairs and arbitrarily big terms in conditions.\"","\"We discuss \"\"completion\"\" methods to generate convergent conditional rewrite systems equivalent to a given set of conditional equations. Finally, we study equation solving methods and formulate a goal-directed approach that improves prior methods and detects more unsatisfiable equations.\"","Made available in DSpace on 2011-05-07T14:00:13Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 8924945.pdf: 3418662 bytes, checksum: 7091f62f07b3e26ed8cd2d1da41a6b6a (MD5) Previous issue date: 1989","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T15:01:48Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:29:21-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"]},{"key":"dc:title","label":"Title","values":["Proofs and computations in conditional equational theories"]}]}],"canonical_facts":{"dc:contributor":["Dershowitz, Nachum"],"dc:creator":["Sivakumar, G."],"dc:date":["2011-05-07T14:00:13Z","10000-01-01","1989"],"dc:description":["Conditional equations arise naturally in the algebraic specification of data types. They also provide an elegant computational paradigm that cleanly combines logic and functional programming. In this thesis, we study how to do proofs and computations in conditional equational theories, using rewriting techniques.","\"We examine different formulations of conditional equations as rewrite systems and compare their expressive power. We identify a class of \"\"decreasing\"\" systems for which most of the basic notions (like rewriting and computing normal forms) are decidable. We then study how to determine if a conditional rewrite system is \"\"confluent.\"\" We settle negatively the question whether \"\"joinability of critical pairs\"\" is, in general, sufficient for confluence of terminating conditional systems. We also prove two positive results for systems having critical pairs and arbitrarily big terms in conditions.\"","\"We discuss \"\"completion\"\" methods to generate convergent conditional rewrite systems equivalent to a given set of conditional equations. Finally, we study equation solving methods and formulate a goal-directed approach that improves prior methods and detects more unsatisfiable equations.\"","Made available in DSpace on 2011-05-07T14:00:13Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 8924945.pdf: 3418662 bytes, checksum: 7091f62f07b3e26ed8cd2d1da41a6b6a (MD5) Previous issue date: 1989","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T15:01:48Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:29:21-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"],"dc:identifier":["AAI8924945","(UMI)AAI8924945","http://hdl.handle.net/2142/23046"],"dc:language":["eng"],"dc:rights":["Copyright 1989 Sivakumar, G."],"dc:subject":["Computer Science"],"dc:title":["Proofs and computations in conditional equational theories"],"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:21Z"}