Satisfiability Problem · Formal Verification and Proof Systems

Lesson 4

Nikolai Chukhin · Alexander S. Kulikov

Let us show how in the resolution proof system one can prove the unsatisfiability of the formula \[\texttt{[-1, -2, -3] [1, -2] [2, -3] [3, -1] [1, 2, 3]}\] in six steps:

  1. \(\texttt{[\textcolor{#90ee90}{-1}, -2, -3] [\textcolor{#90ee90}{1}, -2]}\) \(\Rightarrow\) \(\texttt{[-2, -3]}\)
  2. \(\texttt{[\textcolor{#90ee90}{-2}, -3] [\textcolor{#90ee90}{2}, -3]}\) \(\Rightarrow\) \(\texttt{[-3]}\)
  3. \(\texttt{[\textcolor{#90ee90}{3}, -1] [\textcolor{#90ee90}{-3}]}\) \(\Rightarrow\) \(\texttt{[-1]}\)
  4. \(\texttt{[\textcolor{#90ee90}{-3}] [1, 2, \textcolor{#90ee90}{3}]}\) \(\Rightarrow\) \(\texttt{[1, 2]}\)
  5. \(\texttt{[1, \textcolor{#90ee90}{2}] [1, \textcolor{#90ee90}{-2}]}\) \(\Rightarrow\) \(\texttt{[1]}\)
  6. \(\texttt{[\textcolor{#90ee90}{-1}] [\textcolor{#90ee90}{1}]}\) \(\Rightarrow\) \(\texttt{[]}\)