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.