Abstract
A proposal is made for a formal framework in which equational provability can be represented and investigated. The basic formalism is an algebra of binary relations on ground terms of a first-order language. Two special-purpose mappings are introduced to deal with the structure of terms. Equational provability is characterized in terms of least fixpoints of some mappings. The use of the relational framework is illustrated by a few examples. It is shown that provability of an equation from a finite set of equations, where all equations are variable-free, is decidable. Then we discuss a method by Reeves ([3]) to deal with equations in semantic tableaux, that we can now prove to be complete in a very simple way. Finally, we discuss an equational proof format that is naturally induced by the relational formulation and serves as a guideline in finding proofs. The relation between Reeves' rules and the construction of such proofs is made explicit.
Get full access to this article
View all access options for this article.