The System for Automated Deduction can check validness of a ForTheL-proposition in the context of 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 first window below and a ForTheL-proposition (or a single affirmation) in the second window. Use the command [Parse] to see the translation of your ForTheL input to the first-order language. Use the commands [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 lemma of the nonstandard analysis. [Try this example]

2. A lemma about binary relations. [Try this example]

3. Halting problem. [Try this example]

4. Schubert's Steamroller problem. [Try this example]