The System for Automated Deduction can verify a self-contained ForTheL-text. You can find a brief introduction to ForTheL and some examples of a ForTheL-text on the Explanations page.

Enter a ForTheL-text in the window below. Use the command [Parse] to see the translation of your ForTheL-text to the first-order language. Use the command [Prove] or [Prove with SPASS] to launch verification. If the 'verbose' option is set, you will get a lot of technical information (clauses, proof trees, etc) so you might want to leave it unset. The settings 'Time limit', 'Initial depth bound', and 'Final depth bound' control the process of inference search by the prover of SAD. Turn on 'Equality handling' if your problem contains the equality predicate without the axioms of equality (Brand's modification method is used). When SPASS is used, only the time limit setting is taken into account.

1. A simple text about empty sets. [Try this example]

2. Basic properties of a natural number ordering. [Try this example]

3. Infinite and Finite Ramsey Theorems. [Try this example]

4. The square root of a prime number is irrational. [Try this example]