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

The System for Automated Deduction can verify 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 window below. Use the command [Parse] to see the translation of your ForTheL text to the first-order language. Use the command [Prove with Moses] or [Prove with] to launch verification.


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

  2. Basic arithmetical properties. [Try this example]

  3. Tarski's Fixed Point Theorem. [Try this example]

  4. Newman's Lemma. [Try this example]

  5. Chinese Remainder Theorem. [Try this example]

  6. Infinite Ramsey Theorem. [Try this example]

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

  8. Cauchy-Bouniakowsky-Schwartz inequality for real vectors. [Try this example]

  9. Fuerstenberg's proof of the infinitude of primes. [Try this example]

to Russian Last modified: 3 Aug 2008