Deductive Computer Programming. Revision
Abstract
In an effort to make the research accessible to a wider audience besides the scholarly journals, the PI has published two volumes of the book 'The Logical Basis of Computer Programming'. This book requires only an intuitive understanding of sets, relations, functions, and numbers. Despite the elementary approach, the text presents some novel research results, including: theories of strings, trees, lists and finite sets which are particulary suited to theorem-proving and program-synthesis applications; formalization of parsing; a nonclausal version of skolemization; a treatment of mathematical induction in the deductive-tableau framework. The implemented tableau system combines features lacking elsewhere such as producing proofs by mathematical inducing.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1989
- Accession Number
- ADA219848
Entities
People
- Zohar Manna
Organizations
- Stanford University