Proof Rondo 1.1 (preview)

First-order logic proof checker, now with named lines, axioms, lemmas and definitions

Original: Proof Rondo by H. Basold and J. van Leenen · gitlab.com/hbasold/proof-rondo

This version: named lines, axioms, lemmas and definitions, by R. F. Cunha · gitlab.com/rafaelcunha2013/proof-rondo (branch demo)

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

Proof Input

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

Output

Result

Settings

Strictness:
Restrict to signature:
ℱ ℛ