Find Equational Proofs in Boolean Logic

The function FindEquationalProof can construct a proof of a theorem from a set of axioms if they are all expressed in equational form, that is, equalities between formulas built from the operators of the theory.

Use AxiomaticTheory to obtain a collection of axioms for a theory, like Boolean logic. You can specify the names of the operators and constants involved. Bound variables are represented using formal symbols like a, b, c.

Construct a proof of an equation.

Display the proof as a graph showing the flow of lemmas proceeding from the axioms (green squares) to the conclusion (red square). Triangles and circles represent different types of lemmas.

Alternatively, display all details about the proof steps.