zbMATH — the first resource for mathematics

Bi-rewrite systems. (English) Zbl 0865.68070
Summary: We propose an extension of term rewriting techniques to automate the deduction in monotone pre-order theories. To prove an inclusion \(a\subseteq b\) from a given set \(I\) of them, we generate from \(I\), using a completion procedure, a bi-rewrite system \(\langle R_\subseteq,R_\supseteq\rangle\), that is, a pair of rewrite relations \(@>>{R_\subseteq}>\) and \(@>>{R_\supseteq}>\), and seek a common term \(c\) such that \(a@>*>{R_\subseteq}>c\) and \(b@>*>{R_\supseteq}>c\). Each component of the bi-rewrite system \(@>>{R_\subseteq}>\) and \(@>>{R_\supseteq}>\) is allowed to be a subset of the corresponding inclusion relation \(\subseteq\) or \(\supseteq\) defined by the theory of \(I\). In order to assure the decidability and completeness of such proof procedure we study the termination and communication of \(@>>{R_\subseteq}>\) and \(@>>{R_\supseteq}>\). The proof of the commutation property is based on a critical pair lemma, using an extended definition of critical pair. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. Although we center our attention on the completion process à la Knuth-Bendix, the same notion of extended critical pairs is suitable to be applied to the so-called unfailing completion procedures. The completion process is illustratred by means of an example corresponding to the theory of the union operator. We show that confluence of extended critical pairs may be ensured adding rule schemes. Such rule schemes contain variables denoting schemes of expressions, instead of expressions. We propose the use of the linear second-order type \(\lambda\)-calculus to codify these expressions schemes. Although the general second-order unification problem is only semi-decidable, the second-order unification problems we need to solve during the completion process are decidable.

68Q42 Grammars and rewriting systems
Full Text: DOI