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]