For atomic sentences, use P, Q, R, etc.

For premises, use “Premise” or “P” as citation.

For axioms, use “PL1”, “PL2” or “PL3” as citation.

For modus ponens, use “MP;1,2” (e.g.) as citation.

Line Return or Control + “l” key: checks the line.

Row Control + “r” key: adds row below.

Row Control + “d” key: deletes current row.

Entire proof Control + “p” key: checks entire proof.

PL Proof Machine

Messages

PL