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.
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).
C.-L. Chang and C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving, chapter 5. Academic Press, 1973.