Automated deduction, CADE-19: 19th International Conference by Franz Baader

Show description

G(x1 , . . , xj−1 , zik , xj+1 , . . , xm ) ] / V(D) for all i. , n}, zi ∈ be the set of rules used in this reduction and let Var g,f (α) = {i | xi ∈ V(D)}. With exceptions, now dbl is also compatible with “+” and len is compatible with app. Note that in Def. 8, g can also be a symbol of FT . For instance, s is compatible with len. We obtain C = 0 and D = s(0) for α1len and C = D = s(✷) for α2len . So for both len-rules α, Rule s,len (α) = ∅ and Var s,len (α) = ∅. Similarly, in Ex. 2, “+” is compatible with “∗” on argument 1 and on argument 2.

Fd is a compatibility sequence on arguments j1 , . . ,fd (α) = ∅, for all 1 ≤ i ≤ d − 1 and all fd -rules α ∈ / Exc fd−1 ,fd ∗ • r = f1 (p∗1 , f2 (p∗2 , . . fd−1 (p∗d−1 , fd (x∗ , qd∗ ), qd−1 ) . . , q2∗ ), q1∗ ), ∗ where x are variables on fd ’s inductive positions which do not occur elsewhere in r, and fi (p∗i , fi+1 (. ), qi∗ ) |ji = fi+1 (. ) for all 1 ≤ i ≤ d − 1 • Rule fd (α) = {α} and Pos fd (α) = {i | V(si ) ∩ V(C) = ∅, i non-inductive}, for all fd -rules α : fd (s1 , . . ), . . ,fd (α)}, / Exc fd−1 ,fd for all 1 ≤ i ≤ d − 1 and all fd -rules α ∈ Whether f1 , .

Finally, the decision procedure of the underlying theory can be used to decide the validity of the resulting formulas. 3 Compatibility among Function Definitions Our criteria for decidable equations rely on the notion of compatibility between T -based functions. Definition 7 (T -based Function [12]). A function f ∈ F is T -based iff f ∈ FT or if all rules l → r ∈ R with root(l) = f have the form f (s∗ ) → C[f (t∗1 ), . . , f (t∗n )], where s∗ , t∗1 , . . , t∗n are from Terms(FT , V) and C is a context over FT .