Title :
Proof by consistency in equational theories
Author_Institution :
Dept. of Comput. Sci., State Univ. of New York, Stony Brook, NY, USA
Abstract :
A method is proven for proving that equations are valid in the initial model of an equational variety. This proof by consistency procedure can be applied to equational theories that are represented as ground convergent rewrite systems. In contrast with so-called inductive completion procedures, the method requires no specific ordering on terms and can handle unorientable equations. The method is linear and refutationally complete, in that it refutes any equation which is not an inductive theorem.<>
Keywords :
theorem proving; equational theories; ground convergent rewrite systems; proof by consistency; Algebra; Computer languages; Computer science; Equations; Logic functions; Terminology;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5122
