SAD system Explanations Download Our Team
Inference Search Theorem Proving Text Verification TPTP Problems

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]

to Russian Last modified: 11 Oct 2007