Система Автоматизации Дедукции может проверить корректность замкнутого ForTheL-текста. Краткое введение в ForTheL и примеры ForTheL-текстов даны на странице Пояснения.

Введите входной ForTheL-текст в окне внизу. Команда [Parse] возвращает перевод входного ForTheL-фрагмента в язык первого порядка. Команды [Prove with Moses] и [Prove with] запускают верификацию.

1. Простой текст из теории множеств. [Запустить пример]

2. Простые арифметические утверждения. [Запустить пример]

3. Теорема Тарского о неподвижной точке. [Запустить пример]

4. Лемма Ньюмена. [Запустить пример]

5. Китайская теорема об остатках. [Запустить пример]

6. Бесконечная версия теоремы Рамсея. [Запустить пример]

7. Иррациональность квадратного корня из простого числа. [Запустить пример]

8. Неравенство Коши-Буняковского для вещественных векторов. [Запустить пример]

9. Теорема Фюрстенберга о бесконечности множества простых чисел. [Try this example]