Resolution completeness proof source

[kach]

I was wondering where the proof described in http://www.mathcs.duq.edu/simon/Fall04/notes-6-20/node3.html came from. It's a clever argument, and it seems different from the one in Russell and Norvig, this one (http://arxiv.org/pdf/cs/0606084.pdf), and even Robinson's original proof (free subset http://www.researchgate.net/publication/220431038_A_Machine-Oriented_Logic_Based_on_the_Resolution_Principle).

Do, by any chance, have a source (a paper, textbook, or even original author)? :-)

EDIT: Here's another proof that uses forcing…

[RyanMarcus]

I don't! To be perfectly honest, I Google searched and linked to the first proof that reminded me of the one I learned while I was at the University of Arizona. I learned it in my symbolic logic class, where we used this textbook: http://www.amazon.com/Mathematical-Introduction-Logic-Second-Edition/dp/0122384520

I imagine I personally first saw the proof in there. Perhaps the text will have a reference? I don't have the book with me where I'm currently living, so I'm unable to check. It's also possible our professor just threw it up on the board one day for fun...

I'll try to look into this more later.

[kach]

So exploring the math behind Vulcan inspired me to write my own theorem prover, which I've been working on for the past couple of months. I tried to extend it to support first-order logic. Current progress is here (and I'm working on a series of articles explaining how it works here). Thought you might enjoy looking at this.

Thanks again for a great intro to resolution theorem proving—I discovered so much cool math because of your blog post! :-)

[RyanMarcus]

Neat! I was getting there, but I didn't quite have time to go through all the Skolemization stuff... I'm going to read through your stuff soon.