The System for Automated Deduction can verify a selfcontained 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 firstorder language. Use the command [Prove with Moses] or
[Prove with] to launch verification.
Examples:
 A simple text about empty sets.
[Try this example]
 Basic arithmetical properties.
[Try this example]
 Tarski's Fixed Point Theorem.
[Try this example]
 Newman's Lemma.
[Try this example]
 Chinese Remainder Theorem.
[Try this example]
 Infinite Ramsey Theorem.
[Try this example]
 The square root of a prime number is irrational.
[Try this example]
 CauchyBouniakowskySchwartz inequality for real vectors.
[Try this example]
 Fuerstenberg's proof of the infinitude of primes.
[Try this example]
