RELATIONAL ALGEBRA AND EQUATIONAL PROOFS

Article type: Research Article

Authors: de Kogel, Eric

Affiliations: Co-operation Centre Tilburg and Eindhoven Universities (SOBU), c/o Tilburg University, P.O. Box 90153, 5000 LE Tilburg, The Netherlands. e-mail [email protected]

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.

DOI: 10.3233/FI-1995-2315

Journal: Fundamenta Informaticae, vol. 23, no. 1, pp. 101-121, 1995