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 ForTheL texts 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 with Moses] or [Prove with] to launch verification.

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]