This is a classical propositional logic prover. First, it provides the number of countermodels for the input formula. Second, via Quine's algorithm, it provides a proof that the input formula either a tautology, or an antilogy, or neither one nor the other. To remind the rules used by Quine's algorithm, go to this web page.
Syntax for input formulas
| 0 | 1 | A | ~ A | A & B | A v B | A => B | A <=> B |