Enter clause data
Write one clause per line. Separate literals using commas, v, ∨, OR, or |. Use ~, !, -, or ¬ for negation.
Example data table
| Scenario | Premises | Query | Expected outcome |
|---|---|---|---|
| Implication chain | { P ∨ Q } { ~P ∨ R } { ~Q ∨ R } |
{ R } | Entailed after adding { ~R } and deriving □. |
| Consistent set | { A ∨ B } { ~A ∨ B } |
None | Satisfiable because closure ends without the empty clause. |
| Direct contradiction | { X } { ~X } |
None | Unsatisfiable because resolution immediately derives □. |
Formula used
The calculator applies the classical propositional resolution rule. If one clause contains a literal and another contains its complement, the complementary pair is removed and the remaining literals are merged.
(A ∨ B) and (~A ∨ C) ⟹ (B ∨ C)
For entailment, the tool uses refutation. It adds the negation of the query clause to the premises, then tries to derive the empty clause □. Deriving □ means the original premises logically entail the query. Failure to derive □ after full closure means the query is not entailed.
How to use this calculator
- Choose Entailment by contradiction or Satisfiability only.
- Enter premises in conjunctive normal form, using one clause per line.
- Separate literals with commas, v, ∨, OR, or the pipe symbol.
- Use ~P, !P, -P, or ¬P for negated literals.
- Add a single query clause when using entailment mode.
- Set limits for generated clauses and pair checks to control proof size.
- Enable tautology removal or subsumption to keep the search cleaner.
- Submit the form and review the verdict, clause register, and trace table.
- Use the export buttons to download CSV and PDF summaries.
FAQs
1) What does this calculator evaluate?
It evaluates propositional clauses with the resolution rule. You can test satisfiability, inspect derivation steps, or check whether premises entail a target clause.
2) What format should I use for clauses?
Enter one clause per line. Separate literals with commas, v, ∨, OR, or |. Write negation using ~, !, -, or ¬ before the literal name.
3) What does the empty clause mean?
The empty clause, shown as □, represents contradiction. In satisfiability mode it means the set is inconsistent. In entailment mode it means the query follows from the premises.
4) Why is the query negated?
Resolution proves entailment by refutation. The calculator adds the negation of the query to the premises. If this expanded set becomes inconsistent, the original query is entailed.
5) Why are some resolvents skipped?
Skipped rows usually indicate duplicates, tautologies, or clauses already covered by stronger clauses. These checks reduce clutter and help keep the proof search efficient.
6) What is subsumption?
Subsumption means a shorter clause already covers a longer one. For example, {A} subsumes {A ∨ B}. Skipping subsumed clauses can shrink the search space.
7) Can the calculator prove satisfiability?
Yes, when closure completes without producing □. If you stop early because of limits, the outcome becomes undetermined rather than a complete satisfiability proof.
8) Do I need to convert formulas to CNF first?
Yes. The calculator expects clauses already written in clause form. If you start from general formulas, convert them to conjunctive normal form before submitting.