## Instructions

Type a sentence in propositional logic into the input field and press the Solve button. The applet will then convert the given sentence into clause form and use a (very simple) resolution theorem prover to attempt to find a refutation for the given sentence. If the trace box is ticked, it will print a trace of its search into the output window. Since this algorithm can potentially take a long time the Cancel button can be used abandon the search.

The syntax for the input is a KIF-like language. Atoms are words. Non-atomic sentences must be surrounded by brackets and the connective is the first element of such a list. The possible connectives are "not" (which is unary), "and", "or", "=>", and "<=>". Some examples of a syntactically correct input sentences are given below the applet.

## The Applet

 Resolution Theorem Proving Applet (requires Java 1.6)

## Examples

Just copy and paste these into the "Input:" area above. For Mac users, this might not work and they should try selecting and dragging instead.

```(and
(or P Q (not R))
(or P (not Q))
(and (not P) R U))
```
```(and
(or P Q)
(not Q)
(or Q (not P) (not R)))
```
```(and
(or P (not Q))
(or (not P) Q)
(or Q (not R))
(or (not Q) (not R)))
```
```(and
(or P Q)
(or P (not Q))
(or R Q)
(or R (not Q)))
```

More complex examples are a simple problem (inconsistent, solved quickly) and a harder problem (also inconsistent, but too hard for this simple algorithm).

## References

C.-L. Chang and C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving, chapter 5. Academic Press, 1973.