Proof Rondo First-Order Logic Proof Checker

Source: github.com/hbasold/folproof-rondo

Instructions

Enter your proof in the input box below. As you type, a formatted version of your proof will appear on the right, along with a validation status beneath it.

To learn the syntax, explore the examples provided below or refer to the language reference.

Note:
  • The rules for equality are used as = i instead of (Refl) and = e instead of (Repl).
  • Proof Rondo now considers variable assumption (e.g. | with x) part of its line numbering, just like in Logic Rondo.
  • Proof Rondo now has rudimentary support for numerical identifiers. To use a numerical identifier, prefix it with a single quote, e.g. '42.

Proof Checker

Load an example:

Examples:

Proof Input

Note: Press Esc + Tab to escape the proof input.

Output

Result

Settings

Strictness:
Restrict to signature:
ℱ ℛ