S E D K N TI RLA MA N .de/ 9 A R E sb 0 SA FO CK ni- 0 S N Ü .u 2 DE GI BR ags N R w. 23 Jan VERSITÄT HRICHTU 6123SAA MANY W:http://ww NI AC (cid:21)6 ER W ] U F D G W I A . s c [ 1 v 8 0 6 3 . 1 0 7 S4G0A02 9 4 0 4 : 4 v - i 7 X 3 r 4 a 1 N S S I T R A remark on higher order RUE-resolution with O ERUE P E Christoph Benzmüller R - I K Fa hberei h Informatik Universität des Saarlandes, Saarbrü ken, Germany hrisags.uni-sb.de E S SEKI Report SR(cid:21)02(cid:21)05 This SEKI Report was internally reviewed by: Claus-Peter Wirth E-mail: pags.uni-sb.de WWW: http://www.ags.uni-sb.de/~ p/wel ome.html Editor of SEKI series: Claus-Peter Wirth FR Informatik, Universität des Saarlandes, D(cid:21)66123 Saarbrü ken, Germany E-mail: pags.uni-sb.de WWW: http://www.ags.uni-sb.de/~ p/wel ome.html A remark on higher order RUE-resolution with ERUE Christoph Benzmüller Fa hberei h Informatik Universität des Saarlandes, Saarbrü ken, Germany hrisags.uni-sb.de 2002 Abstra t We show that a prominent ounterexample for the ompleteness of (cid:28)rst order RUE-resolution does not apply to the higher order RUE-resolution approa hERUE. Bona inashowsin[BH92℄thatthe(cid:28)rstorderRUE-NRFresolutionapproa hasintrodu edin[Dig79, Dig81, DH86℄ is not omplete. The ounterexample onsists in the following set of (cid:28)rst order lauses: {g(f(a)) = a,f(g(X)) 6= X} X f,g Here is a variable and are unary fun tion symbols. It is illustrated in [BH92℄ that this obviously in onsistent lause set annot be refuted in the (cid:28)rst order RUE-resolution approa h of Digri oli. The extensional higher order RUE-resolution variant ERUE has been proposed in [Ben99b, Ben99a℄ and ompleteness is analyzed in [Ben99a℄. An interesting question is whether the above exampleisalsoa ounterexample tothe ompletenessofERUE.ThetwoERUErefutationspresented below illustrate that this is not the ase. We do not present the ERUE al ulus here and instead refer to [Ben99b, Ben99a℄. In the (A ⇔ B) (A ∧ B) ∨ (¬A ∧ ¬B) followingT we onsidFer as shorthand for . We furthermore use [...] [...] the and -notation of [Ben99a℄ to denote positive and negative literals. Terms are g(f(a)) (g (f a)) presented in the usual (cid:28)rst order style notation, i.e. we write instead of as done in [Ben99b, Ben99a℄. The de omposition rule employed in the refutations below is C ∨[hAn = hVn]F Dec 1 1 F n n F C ∨[A = V ] ∨...∨[A = V ] Thereadermightbemoreusedtothisformofde ompositionthantotheoneemployedin[Ben99b, Dec Ben99a℄. Compared to the latter the above rule also shortens the presentation. The de om- Dec position rule employed in [Ben99b, Ben99a℄ is more general, i.e. rule above is derivable in al ulus ERUE. The (cid:28)rst refutation in ERUE presented below (whi h has been suggested by Chad Brown) FlexRig X employs a (cid:29)ex-rigid uni(cid:28) ation step ( ) in the very beginning. In this key step variable f is bound to an imitation binding that introdu es at head position. The rest of the refutation is then straight forward. 1 2 The se ond refutation shows that there are alternatives to the (cid:29)ex-rigid uni(cid:28) ation step for X [f(a) = variabFle at the beginning. The key idea now is to derive the positive re(cid:29)exivity literal f(a)] C18 in lause . While positive re(cid:29)exivity literals annot be derived in (cid:28)rst order RUE- resolution, our example shows that this is (theoreti ally) possible in ERUE for some symbols and f(a) terms o uring in the given lause ontext, like in our ase. f g We now present both ERUE-refutations in detail. and are still unary fun tion symbols, X H Y while is a variable. and are freshly introdu ed variables. Refutation I T C1 : [g(f(a)) = a] F C2 : [f(g(X)) = X] F F FlexRig(C2): C3 : [f(g(X)) = X] ∨[X = f(H(X))] F Solve(C3) : C4 : [f(g(X)) = f(H(X))] F Dec(C4) : C5 : [g(X) = H(X)] F Res(C1,C5) : C6 : [(g(f(a)) = a) = (g(X) = H(X))] F F Dec(C6) : C7 : [g(f(a)) = g(X)] ∨[a = H(X)] F F Dec(C7) : C8 : [f(a)= X] ∨[a= H(X)] F F Solve(C8) : C9 : [f(a)= f(a)] ∨[a = H(f(a))] F Triv(C9): C10 :[a = H(f(a))] F F FlexRig(C10) : C11 :[a = H(f(a))] ∨[h = λY a] F Solve(C11): C12 :[a = a] Triv(C12): [] Refutation II T C1 : [g(f(a)) = a] F C2 : [f(g(X)) = X] F Res(C1,C2) : C3 : [(g(f(a)) = a) = (f(g(X)) = X)] F Equiv(C3): C4 : [(g(f(a)) = a) ⇔ (f(g(X)) = X)] T T n×Cnf(C4): C5 : [g(f(a)) = a] ∨[f(g(X)) = X] F F C6 : [g(f(a)) = a] ∨[f(g(X)) = X] F F Res(C6,C1) : C7 : [(g(f(a)) = a) = (g(f(a)) = a)] ∨[f(g(X)) = X] F F F Dec(C7) : C8 : [f(a)= f(a)] ∨[a = a] ∨[f(g(X)) = X] F F Triv(C8): C9 : [f(a)= f(a)] ∨[f(g(X)) = X] F F Fac(C9) : C10 :[f(a) = f(a)] ∨[(f(a) = f(a))= (f(g(X)) =X)] F Triv(C10) : C11 :[(f(a) = f(a)) = (f(g(X)) = X)] F Equiv(C11) C12 :[(f(a) = f(a)) ⇔ (f(g(X)) = X)] T T n×Cnf(C12) : C13 :[f(a) = f(a)] ∨[f(g(X)) = X] F F C14 :[f(a) = f(a)] ∨[f(g(X)) = X] T ′ ′ F Res(C13,C2) : C15 :[f(a) = f(a)] ∨[(f(g(X)) = X) = (f(g(X )) = X )] T ′ F ′ F Dec(C15) : C16 :[f(a) = f(a)] ∨[f(g(X)) = f(g(X ))] ∨[X = X ] T ′ ′ F Solve(C16): C17 :[f(a) = f(a)] ∨[f(g(X )) = f(g(X ))] T Triv(C17) : C18 :[f(a) = f(a)] F Res(C2,C18) : C19 :[(f(g(X)) = X) = (f(a)= f(a))] F F Dec(C19) : C20 :[f(g(X)) = f(a)] ∨[X = f(a)] F Solve(C20): C21 :[f(g(f(a))) = f(a)] F Dec(C21) : C22 :[g(f(a)) = a] F Res(C22,C1) : C23 :[(g(f(a)) = a) = (g(f(a)) = a)] Triv(C23) : C24 :[] 3 Theaboverefutationsareadmittedlynon-trivial. Forthisparti ularkindofproblemsparamod- ulation therefore seems to be a more appropriate approa h. However, we suggest a more thorough analysis to su(cid:30) iently larify this question for the higher order ase. A knowledgment: I thank Chad Brown, CMU, Pittsburgh, USA, for his omments and on- tribution. Referen es [Ben99a℄ C. Benzmüller. Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Department of Computer S ien e, Saarland University, 1999. [Ben99b℄ C. Benzmüller. Extensional higher-orderparamodulationand RUE-resolution. In H. Ganzinger, editor, Pro eedings of the 16th International Conferen e on Automated Dedu tion (CADE-16), number 1632 in LNCS, pages 399(cid:21)413,Trento, Italy, 1999.Springer. [BH92℄ M.P.Bona inaandJiehHsiang. In ompletenessoftheRUE/NRFinferen esystems. Newsletter of the Asso iation for Automated Reasoning, No. 20, pages 9(cid:21)12, May 1992. [DH86℄ V. J. Digri oli and M.C. Harrison. Equality-based binary resolution. Journal of the ACM, 33(2):254(cid:21)289,1986. [Dig79℄ V. J. Digri oli. Resolution by uni(cid:28) ation and equality. In W. H. Joyner, editor, Pro . of the 4th Workshop on Automated Dedu tion, Austin, Texas, USA, 1979. [Dig81℄ V.J.Digri oli.Thee(cid:30) a yofrueresolution,experimentalresultsandheuristi theory. InA.Dri- nan, editor, Pro . of the 7th International Joint Conferen e on Arti(cid:28) ial Intelligen e (IJCAI81), pages 539(cid:21)547,Van ouver, Canada, 1981. Morgan Kaufmann, San Mateo, California, USA.