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