Propositional logic concerns concepts such as truth, falsity, conjunction, disjunction, implication, biconditionals, and negation. This page serves as an index for proof modules and interfaces in this area.
Intuitionistic logic is a subsystem of classical logic which is sometimes used in its own right, and which here provides the proofs for many of the propositional logic theorems.
By adding the law of the excluded middle to intuitionistic logic, we get classical logic.
There are a variety of theorems which are fairly direct consequences of the above theorems but which exist to simplify proofs which use them.