Abstract :
We consider a constrained equational logic where the constraints are membership conditions t swheresis interpreted as a regular tree language. Our logic includes a fragment of second-order equational logic (without projections) where second-order variables range over regular sets of contexts. The problem with constrained equational logics is the failure of the critical pair lemma. This is the reason why we propose new deduction rules for which the critical pair lemma is restored. Computing critical pairs requires, however, solving some constraints in a second-order logic with membership constraints. In a second paper we give a terminating set of transformation rules for these formulas, which decides the existence of a solution, thus showing a new term scheme unification algorithm.
Since an order-sorted signature is nothing but a bottom–up tree automaton, order-sorted equational logic falls into the scope of our study; our results show how to perform order-sorted completion without regularity and without sort-decreasingness. It also shows how to perform unification in the order-sorted case, with some higher-order variables (without any regularity assumption).
