Resolution Tool
Description
This is a tool designed to help you understand the concept of resolution. The
conjunctive normal form
of the formula is generated and its clauses displayed in a list. You can create new
clauses by
resolving clauses in the list.
Instructions
Enter a formula in the top box below.
Click on the "CNF" button.
The conjunctive normal form of the formula will be displayed in the
bottom box below.
The clauses of the formula are displayed beneath.
Tick the boxes next to two of the formulae to resolve them.
An atom can be any string consisting of one or more letters.
Use the following symbols for the logical connectives:
| ^ | (and) |
| v | (or) |
| => | (implication) |
| <=> | (equivalence) |
| ~ | (not) |
|