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, the formatted proof will appear on the right, along with a validation status, beneath that. To learn the syntax, try playing with the examples, below, or see the language reference.

Note:
  • There is currently a limitation in the parser, where the last substitution quantifier rules cannot contain spaces. Thus, you have to write x/g(c,d) instead of x/g(c, d)!
  • The rules for equality are used as = i instead of (Refl) and = e instead of (Repl).

Proof Checker

Load an example:

Examples:

Proof Input

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

Output

Result

Settings