Scunak

Javascript Interactive Higher-Order Theorem Prover

Math Gate

Automated Reasoning in Higher Order Logic

Automated Reasoning in Higher Order Logic

This page was created and is maintained by Chad E Brown.

Axiom Schemas for Andrews' System P for propositional logic (Keep in mind disjunction and negation are the only primitives. The other connectives are abbreviations.)

Axiom Schema 1. A or A implies A

Axiom Schema 2. A implies . B or A

Axiom Schema 3. A implies B implies . C or A implies . B or C

Rule of Inference:

Modus Ponens. From A and not A or B we can infer B.