Elysian Shadows

For my AI class...
I need to create ground clauses (sentences with no variables, all terms separated by OR) to prove a contradiction (like Q AND !Q) from
where C is a constant symbol
R(C)
!R(f(C))
R(f3(C))
[1] R(x) v !R(f3(x))
[2] !R(x) v R(f2(x))

Where f# simply is shorthand for f( f( ... ) ) # times [so f2(x) is f(f(x))]
The original is at
http://www.cs.uky.edu/~mirek/class-mate ... hmwk-8.pdf #2, the first question regarding it.
The f2 gives me trouble. I want to say, like, (don't think I can even do this though)
[2] !R(x) v R(f2(x)) gives me !R(f(C)) v R(f3(C))
because I couldn't get anywhere with
!R(C) v R(f2(C)) but maybe I was doing it wrong.

And then if I used
[1] R(x) v !R(f3(x)) to give, say, R(C) v !R(f3(C)) ... well, I wind up with !R(f(C)) and R(C) which are both given as true, when I need to prove false ...

But R(f(C)) v !R(f4(C)) from [1] leaves me with an f4. Which is f2(f2(C)) where f2(.. is what, D? I dunno. A guide in the right direction would be nice.

Also I need to get this question right so I can get a high enough grade on the hw to get an A in the class and be exempt from the final :(

thats AI, lookst like dicreet math to me. i havent done that for years. i might have a solution manual for you.

I haven't found his exact problems anywhere else on the internet.

i have a teachers sulotion manual. i might not get the specific one, but something close.

im looking, here is some links that might help.

http://www.philosophypages.com/lg/e11a.htm
http://www.mathpath.org/proof/proof.inference.htm
http://www.cs.odu.edu/~toida/nerzic/con ... infer.html

you have to first make a premis, then
you need to use inference rules to make the statements say something else.
and equate it to your premist.

and add QED. lolz, (little joke im not sure if you'll get it.)

I'm assuming R is a relation, is it valid for me to ground x as !R(C), for instance?
Edit: Ah, I have to use resolution (essentially AND things together) to obtain a contradiction, and I have to ground all clauses (make them have no variable symbols, since the clauses given are universally quantified), per problem. My hitch is what to ground x as.
Sorry, I didn't rewrite the entire thing. But I think that covers the rest of it.

Something like this. I'm not sure I can ground x with a relation [R] (sort of think that I can't)...

Or... is it possible for me to put two different things in for two different x's in the same clause? I don't think so, right?

Edit: Also, for the second part of #2, if someone knows how to resolve with unification ({a/b} reads as "use a for b") or wants some other example of resolution, I'm pretty confident on this one (this also involves the 'standardize variables apart' where you rename variables that you resolve together, so the x's are renamed to something that the formula they're being resolved into does not have)

Okay, I think this is it
(x as C, x as f(C), x as C, x as f2(C). Grounded them twice: should be valid since these are for all x)

WTF is that?! Lol.. good luck man.

That was it. I got a 100 on this homework (and a 94 in the class, A, exempt from final).

Congratulations Marauder!