Prove a theorem in first-order logic:

Show the theorem statement:

Show the complete list of proof steps as a Dataset object:

Show the abstract proof network:

Prove a theorem in first-order logic:

Show the theorem statement:

State the axioms of the theorem:

Show the type of logic used:

Show the complete list of proof steps as a Dataset object:

Show the abstract proof network:

Typeset a natural language argument:

Build a function that performs the steps of the proof:

Specify the axioms of group theory:

Prove the existence of the left identity:

Show the theorem statement:

State the axioms of the theorem:

Show the type of logic used:

Specify the axioms of abelian group theory:

Prove a theorem in abelian group theory:

Show the proof dataset:

Extract the statement of Critical Pair Lemma 2:

Extract the proof of Critical Pair Lemma 2:

Specify some short axioms for Boolean logic:

Prove a theorem in Boolean algebra:

Show the abstract proof network:

Highlight all of the substitution lemmas:

Prove a theorem in first-order logic:

Typeset a natural language argument:

Specify the axioms of Sheffer logic:

Prove a theorem in Sheffer logic:

Build (and run) the associated proof function: