Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
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
add comment

1 Answer

up vote 1 down vote accepted

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

share|improve this answer
    
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.