# The resolution method

how do I find the resolvent of this formula?

$(A \vee C) \wedge ( \neg A \vee B) \wedge C$

Is it as easy as taking every clause with the same statements?

$(A \vee C)$ and $( \neg A \vee B)$ and put out the contradiction (in this case $A$ and $\neg A$)

Could you recommend me some source for resolution method except Wikipedia, because there are too easy examples?

-
Try Googling "resolution proof system". –  Yuval Filmus Dec 5 '10 at 23:52
The version of resolution I'm aware of is a proof system for refuting a conjunction of clauses, but your formula is not contradictory. In fact, it is a 2-SAT formula and so there's a simple efficient algorithm for deciding whether it's satisfiable. –  Yuval Filmus Dec 5 '10 at 23:53

## 1 Answer

Yes, you're going to find clauses with contradictory literals and apply the resolution rule to those. So you're going to resolve the first two clauses in your example.

Here are a couple of pages you can look at:

http://www.ai.mit.edu/courses/6.825/fall02/pdf/6.825-lecture-07.pdf

http://logic.stanford.edu/classes/cs157/2005/notes/chap05.pdf

-
Thanks for usefull sources at MIT and Stanford... I can't believe, our university is keeping similar materials only for their students and teachers even it's not as good (self-explaining) as materials from MIT/Stanford :D –  Radek Simko Dec 6 '10 at 9:02