Lisp Inference Truth Table System

+------------------------+
|  P  |  Q  |  (P => Q)  |
+------------------------+
|  T  |  T  |     T      |
|  T  |  F  |     F      |
|  F  |  T  |     T      |
|  F  |  F  |     T      |
+------------------------+

Operators: (~ ^ <=> => -> <-> V [+])

Some notes:

• Please, don't be evil. Use less than 10 variables.

• Use spaces around operators. Use 'p ^ q' instead 'p^q'.

• Yes, [+] it's a XOR. Mathematically: p ⊕ q.

• (=> ->) and (<=> <->) are aliases.

Tautologies:

• de morgan: ~p v ~q <=> ~(p ^ q)
• modus ponens: p ^ (p -> q) => q
• constructive dilemma: ((p -> q) ^ (r -> s) ^ (p v r)) => (q v s)
• hypothetical syllogism: ((p -> q) ^ (q -> r)) => (p -> r)
• disjunctive syllogism: ((p v q) ^ ~p) => q
• implication: p -> q <=> ~ p v q