A theorem checker for the formal system P that describes propositional logic.
The alphabet of propositional logic includes:
- propositional variables: a, b, c, ..., z
- connectives: ¬, ∨. derived connectives: ->, <->, ∧,
- parentheses: (, )
The set of formulas FOR of propositional logic is defined inductively and is the smallest set that satisfies the following rules:
- Every propositional variable p is a formula.
- If p and q are formulas, then ¬p, (p ∨ q), (p -> q), (p <-> q) and (p ∧ q) are formulas.