University of Illinois Urbana-Champaign

Proofs and computations in conditional equational theories

Sivakumar, G.

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/23046

Description

Title
Proofs and computations in conditional equational theories
Author(s)
Sivakumar, G.
Issue Date
1989
Doctoral Committee Chair(s)
Dershowitz, Nachum
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
  • 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."
Type of Resource
text
Permalink
http://hdl.handle.net/2142/23046
Copyright and License Information
Copyright 1989 Sivakumar, G.

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer Science