Type a sentence in propositional logic into the input field, select the type of normal form desired, and press compute. The applet will then convert the given sentence into CNF or DNF and display the result.
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 "<=>". An example of a syntactically correct sentence is:
(=> (and P Q) (<=> R (not S)))
C.-L. Chang and C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving, chapter 2. Academic Press, 1973.