Proofly

Learn digitally to argue mathematically.

Try a proof

Prototype

Proofly is a work in progress.

A first prototype is already available for a selection of proof methods — here is one of them.

Equivalence transformations

Equivalence of First-Order Logic Formulas

The Proofly editor: a block palette on the left, and a proof workspace where one first-order formula is rewritten step by step into the other, each step naming the equivalence applied.

What you practise

Showing that two formulas are equivalent: rewrite one of them step by step, and name the equivalence you apply at each step until the other formula stands there.

Try this exercise →