1
$\begingroup$

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?

  • 0
    Try Googling "resolution proof system".2010-12-05
  • 0
    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.2010-12-05

1 Answers 1

1

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

  • 0
    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 :D2010-12-06