Proof using resolution refutation

27 Views Asked by At

I am trying to prove my goal, LIKE(Anna), and I am wondering if I can use the goal several times in the proof? I begin by negating the goal, ~LIKE(ANNA). I have 6 different clauses I can use. I begin with LIKE(Casper)|~BADGRADES(CASPER) and the negated goal ~LIKE(ANNA). After applying 3 other (different) clauses, I end up with LIKE(x). I am wondering if I can reuse the negated goal here ~LIKE(ANNA), to end up with NIL, or is that not allowed after using it in the first step? In the end I have used the goal twice and 4/6 clauses.