Equational formulae with membership constraints (Q1333268): Difference between revisions

The ``automated'' transformation of equational formulae into ``simpler'' forms has many applications (functional and logic programming; abstract data types; automated deduction, a.s.o.). The formal framework is given by equational formulae in order-sorted algebras. The equational formulae are here first-order logical formulae whose atoms are either equations (\(t=s\), where \(t\) and \(s\) are terms over an order-sorted signature), or membership constraints (\(t\in \tau\), where \(t\) is a term and \(\tau\) is a sort). A solved-form of an equational formula represents either \(\perp\) (meaning ``no solution'') or a most general unifier (a solution of the considered formula), having the same syntactical form. In the chosen context, solvability is decidable and a correct set of transformation (rewriting) rules is provided. ``The main results are termination and completeness of our set of rules''. Quantifier elimination is also treated. The last part of the paper is devoted to the study of some applications and consequences (such as the axiomatization of a structure describing a regular tree language, or automatic proofs by induction in equational theories). A preliminary version by the first author of this work appeared in the Proceedings of the ICALP 1990, under the title ``Equational formulas in order-sorted algebras'' [Lect. Notes Comput. Sci. 443, 674-688 (1990; Zbl 0774.68071)].