1990 | ReviewPaper | Chapter
Proving and rewriting
Author : Joseph A. Goguen
Published in: Algebraic and Logic Programming
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper presents some ways to prove theorems in first and second order logic, such that rewriting does the routine work automatically, and partially successful proofs often return information that suggests what to try next. The theoretical framework makes extensive use of general algebra, and main results include an extension of many-sorted equational logic to universal quantification over functions, some techniques for handling first order logic, and some structural induction principles. The OBJ language is used for illustration, and initiality is a recurrent theme.