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 |
that corresponds to the usual symbolism:
|\(\bot\) | \(\top\) | \(A\) | \(\lnot A\) | \(A \land B\) | \(A \lor B\) | \(A \to B\) | \(A \leftrightarrow B\) |
Do not write a => b, but A => B .
proof will show here