0

For simpler questions involving proof by resolution, it is easy to see whether or not a contradiction can be found by inferring the empty clause, and somewhat easy to show there is no empty clause inference. However, for questions involving a larger number of clauses and terms, such as:

$a ∨ b ∨ c \\ a ∨ ¬c ∨ d \\ ¬a ∨ e ∨ f \\ c ∨ ¬e ∨ f \\ c ∨ ¬d ∨ ¬f $

How exactly, using a formal method, can we show that an empty clause cannot be inferred?

zzxxx123
  • 113
  • Case distinction? – Dirk May 07 '19 at 10:44
  • What do you mean? Try every possible case? – zzxxx123 May 07 '19 at 10:53
  • In a clever way, of course, but yes. That is sometimes the best way to go, like "case 1: $a = 0$, case 1a $b \neq 0$,...". It doesn't look as elegant as other proofs, but it is a systematic way to get things done. – Dirk May 07 '19 at 10:57
  • Checking that the set of clauses is satisfiable. Set $a= \text T$ and the two first clauses are sat. Then with $f= \text T$ also the third and fourth are. And it's done. – Mauro ALLEGRANZA May 07 '19 at 11:06

0 Answers0