Topics in Automated Theorem Proving and Program Generation
Hsiang, Jieh
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/69514
Description
Title
Topics in Automated Theorem Proving and Program Generation
Author(s)
Hsiang, Jieh
Issue Date
1983
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
Abstract
This thesis contains two parts, each deals with a different subject.
PART I: Automated Theorem Providing. Effective theorem provers are essential for automatic verification and generation of programs. The conventional resolution strategies, albeit complete, are inefficient. On the other hand, special purpose methods, such as term rewriting systems for solving word problems, are relatively efficient but applicable only to small classes of problems.
In this thesis, a simple canonical set of rewrite rules for Boolean algebra is presented. Based on this set of rules, the notion of term rewriting systems is generalized into complete proof strategies for first order predicate calculus. The methods are conceptually simple and can frequently utilize lemmas in proofs. Morever, when the variables of the predicates involve some domain which has a canonical system, the system can be added as rewrite rules, and algebraic simplifications can be done simultaneously with the merging of clauses. This feature is particularly useful in program verification, data type specification, and programming language design, where axioms can be expressed as equations (rewrite rules). The methods are being implemented, and preliminary results indicate that they are space-efficient with respect to the number of rules generated (as compared to the number of resolvents in resolution provers).
PART II: Deductive Program Generation. A deduction system which expresses programs as proofs is given. In this system, one gives assertions describing the algorithm and derives a statement of the form: "There is a program P satisfying the input/output relation". From this proof, the program can be extracted mechanically in any high level language. The system provides a method of algorithm specification at a high degree of abstraction and generality, since its syntax is independent of any particular programming language. It can also be used as a very high level programming language. The method provides a natural formalism for describing programs with multiple exits, and a natural way of combining pieces of programs into larger ones. Some examples are given, and comparisons are made with other logic based programming approaches.
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.
