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 SAT solver based on Davis and Putnam's algorithm to attempt to find a model for the given sentence. If the trace box is ticked, it will print a trace of its search for a model 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

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 instantly) and a harder problem (also inconsistent, should take about a minute to solve).

References

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