Simplified Resolution Evaluator
This is a simple-minded Resolution evaluator that takes upto 5 clauses, which are disjunctions, and
applies the resolution rule on all pairs until no new resolutions are generated. The way you'd normally
use this technique is to show that a set of clauses, say \(X = X_1 \land X_2 \land \cdots \land X_n\) implies
another, say \(Y\). You'd take the original set of clauses \(X\) and the negation of the implicand \(\neg Y\)
and show that one or more application the resolution inference rule derives \(F\) or \(false\). This would mean
that the set of clauses \(X \land \neg Y\) is unsatisfiable.
Resolution is refutation complete, so if the set of clauses that you start with is unsatisfiable,
then resolution is guaranteed to derive \(F\) starting from that set of clauses.
If \(X \land \neg Y\) is unsatisfiable, then \(X \rightarrow Y\).
Examples
- \(\{\neg p \rightarrow q, p \rightarrow r \lor s, r \rightarrow t \land u, u \land \neg s \rightarrow \neg t\} \models \neg s \rightarrow q\)
— Use resolution.
- Type \(C_1 = p \mid q, C_2 = !q, C_3 = !p\). Note that the set of clauses derives \(F\).
This means that \(p \lor q \land \neg q \rightarrow p\). This makes sense because if
\(p \lor q\) is true and \(q\) is false, then \(p\) must be true.
Type upto 5 clauses (disjunctions) and click submit