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

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

1. Лемма нестандартного анализа. [Запустить пример]

2. Лемма о бинарных отношениях. [Запустить пример]

3. Проблема остановки в теории алгоритмов. [Запустить пример]

4. Задача Л.Шуберта "Паровой каток" (Schubert's Steamroller). [Запустить пример]