The prover takes an S-Expression and returns whether it is a:
- Tautology, returns
T - Satisfiable, returns
Numbersaying how many times it isTrue - Unsatisfiable, returns
U - Invalid S-Espression, returns
E
p -> q: Means If p then q,
which translated into propositional calculus gives: (~p OR q)
A Truth Table for the above example looks like this:
| p | q | ~p | q | ~p OR q (p -> q) |
|---|---|---|---|---|
| F | F | T | F | T |
| F | T | T | T | T |
| T | F | F | F | F |
| T | T | F | T | T |
- NOT
- OR
- IF
- AND
- Support IFF
- Refactor to make it more modular