where ( 2 ! ℄ v℄ expresses that u[s ℄ v is an atom o urring in 2 2)[u[s Let i, q, r, be fun tions, a, b be onstants and be variables x1, x2, x3, x4, y1 j= 2 ! A for all A in 1 NC in general. Therefore, in order to make the rule appli able in pra ti e, it must solely with less sophisti ated redu tion me hanisms su h as unit rewriting or 4: b; i(x1) q(y1) and let r q i b a nil using the KBO with weight 1 for all fun tion 3: a i(x1) is the topi of this paper. subsumption. j= A ! 2 for all A in 1 NC symbols and variables.
For a more sophisti ated, further motivating example, onsider the following lause set. It an be nitely saturated using ontextual rewriting but not from N smaller than C with respe t to a redu tion ordering , total on ground above the bar by the lauses below the bar. Both side onditions are unde idable, be instantiated su h that eventually these two onditions be ome ee tiv e. This where N is the urrent lause set, C; D 2 N , and denotes the set of lauses NC terms. Redu tion rules are labeled with an R and are meant to repla e the lauses or 2 and u ontains the subterm s . Contextual rewriting redu es the subterm 1: s of u to t if, among others, the following onditions are satised 2: b i(x1) sin e no further superposition inferen e is possible. In order to apply ontextual Clause 7 is a tautology and an be redu ed to true. Then the set is saturated 7: b; b; b; b; b a ! nil; a b. i(x1) i(x3) i(x2) q(y1) y1 rewriting we an redu e lause 5 using lause 3 to j= b; b; b; a ! NC i(x1) i(x3) i(x2) q(y1) i(x1) other system we are aware of, an redu e lause However, with ontextual 5.1 rewriting we have to verify the side onditions q( b. (x2; r(x3; y1))) ondition holds trivially and the latter follows from b; b; b; b; b a ! i(x3) i(x2) q(y1) the standard redundan y notion of superposition. A lause C is alled redundant lauses in the form ! where and are multi-sets of atoms. The atoms [5℄ that generalizes unit rewriting and non-unit rewriting [6℄. It is an instan e of in a lause set N if there exist lauses : : : ; 2 N with C for i 2 C1; Cn Ci We onsider rst-order logi with equality using notation from [6℄. We write f1; : : : ; ng, written 2 , su h that : : : ; j= C. The lause C is implied Ci NC C1; Cn or equal than s with respe t to . to literals and lauses in the usual way [6℄. A term s is alled stri tly maximal the bar. in ! if there is no dieren t o urren e of a term in ! that is greater ontextual rewriting rule, are dened with respe t to a well-founded redu tion substitution is a mapping from the set of variables to the set of terms su h that Contextual rewriting is a sophisti ated redu tion rule originally introdu ed in by smaller lauses from N . This ondition an a tually be rened to grounding x 6= x for only nitely many variables x. The redu tion rules, in parti ular the and their appli ation repla es the lauses above the bar with the lauses below i 2 , and : : : ; n j= C . Redu tion rules are marked with an R Ci NC C1 1; Cn are ground instan es i of lauses 2 N su h that i C , written Ci Ci Ci substitutions: C is redundant if for all grounding substitutions for C there ordering on terms that is total on ground terms. This ordering is then lifted of denote negative literals while the atoms of denote the positive literals. A
set, D 2 N , ground, a substitution then the redu tion C0 The redu tion al ulus only needs to redu e ground lauses. There- ‘Red tautologies to true whereas forward subsumption redu es subsumed lauses to working on ground lauses. Further, it adapts ontextual rewriting su h that it exponentially larger than N , in general. Therefore, we represent impli itly NCD a parti ular instan e of ontextual rewriting alled re ursive ontextual ground though this is a de idable approximation of the original problem the set is NCD rules ontaining tautology redu tion, forward subsumption, obvious redu tion and rewriting dened below. Tautology redu tion redu es synta ti and semanti by approximating j= ( ! ) by the appli ation of a redu tion al ulus NCD impli itly onsiders lauses from . NCD ( ! ) >. The redu tion al ulus is omposed of a set of redu tion ‘Red ‘Red fore, the following denition introdu es an instan e of ontextual rewriting only true. Obvious redu tion eliminates trivial literals [6℄. 2. C D 1. s t 5. (A ! > for all A in 2) ‘Red 3. maps all variables from C; D to fresh Skolem onstants 4. ( 2 ! A) > for all A in 1 ‘Red tion and ba kward redu tion whenever a lause is newly generated or modied. ostly to expli itly ompute the Skolem substitution for ea h lause ! erated lauses and ba kward rewriting redu es the previously generated lauses The implementation of Spass [6℄ fo uses on a sophisti ated redu tion ma hinery.
The integration of ontextual rewriting into this ma hinery onsists of two steps. First, the sear h for appropriate ontextual rewrite appli ation andidates ee tiv e implementation of the redu tion al ulus First of all, it is too ‘Red. substitution trees [6, 9℄. indexing [8℄. This fun tionality has already been implemented into Spass via priate ontextual rewrite appli ation andidates an be solved by standard term This ma hinery ompletely interredu es all lauses as it performs forward redu with the new one.
Se ond, validating the side onditions of ontextual rewriting requires an Forward redu tion redu es the newly generated lause using the previously genis analogous to the ase of unit rewriting and non-unit rewriting. In addition, the side onditions of ontextual rewriting have to be he ked. Finding appro
G from N of and the respe tive mat her . Then the pro edure omputes for u0 lause and it requires additional omputations to build the lause. Be ause of Algorithm 1 expe ts as input a lause C and a lause set N and redu es C expli itly requires to allo ate memory for the new onstants and the new subsumed by lauses from N and ObviousRedu tion(C) removes dupli ated explained sense. The all to (N; returns the set of generalizations generalSDT u0) dure is depi ted in Algorithm 1. The algorithm uses tautology deletion, forward assume them to have a lower pre eden e than any other symbol of the signature. subsumption and obvious redu tions from the redu tion pro edure of Spass. The pro edures have to work with respe t to the modied, above explained, orderSpass Handbook [10℄. is the empty lause, IsTautology(C) he ks whether C is either a synta ti or a the idea is to simply treat variables as onstants for this ase. We adapt the on them. In Spass variables are represented by integers whi h impli itly gives As a result, the implementation provides a method for applying to a lause semanti tautology. ForwardSubsumption(C, N) he ks whether C is already the re ursive stru ture of the redu tion al ulus this is not feasible. Therefore, subsumes unit and non-unit rewriting and implements re ursive ontextual ground an ordering on variables. Whenever we onsider variables to be onstants we ings. Besides of this the implementation of these redu tions remains un hanged. rewriting. The variables o urring in C are interpreted as onstants in the above literals and trivial equations from a lause. Further details an be found in the Comparisons between variables are performed on the bases of their integer value. ! without any omputation or memory allo ation. with respe t to N in the main loop. IsEmpty(C) he ks whether the given lause The omposition of the redu tion al ulus to an a tual de ision pro e- ‘Red Re ursiveContextualGroundRewriting(C, N), depi ted in Algorithm 2, ordering modules (KBO, RPOS) su h that they an treat variables as onstants. whi h the redu tion al ulus onsiders for ontextual rewriting. Applying ea h of the generalizations the literals and the lauses where they o ur resulting