Система Автоматизации Дедукции (САД) разрабатывается в рамках исследований по Алгоритму Очевидности. Система предназначена для автоматической обработки формальных математических текстов, записанных в языке ForTheL (FORmal THEory Language). Также допускается ввод в языке первого порядка. Подробные сведения о входных языках САД вы можете получить на странице Пояснения, из примеров секвенций, теорем и текстов, а также из Руководства по языку ForTheL (на английском языке, gzipped PS или PDF).

Система САД распространяется бесплатно с открытым исходным кодом по лицензии GNU GPL. Вы можете загрузить текущую версию САД в виде пакета исходного кода либо пакета исходного кода вместе с исполнимыми файлами (Linux x86, glibc 2.3). Также доступны предыдущие версии САД.

По приведенным ниже гиперссылкам вы можете получить доступ к системе САД в режиме онлайн. Введите ForTheL-текст или секвенцию, предназначенную к обработке, установите параметры поиска вывода и запустите САД. Система обработает задание и вернет результат: перевод ForTheL-текста, дерево доказательства или протокол верификации. Текущая версия системы выполняет следующие задания:

• Поиск вывода:  устанавливает выводимость секвенции первого порядка;
• Доказательство теорем:  доказывает утверждение в контексте заданного ForTheL-текста;
• Верификация текста:  проверяет корректность замкнутого ForTheL-текста;
• Библиотека TPTP:  загружает и доказывает задачу из библиотеки TPTP.

Каждая строка в результирующем выводе "подписана" одним из модулей САД. Модули [ForTheL] и [FOL] отвечают за синтаксический анализ языка ForTheL и первого порядка, соответственно. Модуль [TPTP] обрабатывает задания и наборы аксиом в формате TPTP. Модуль [Reason] управляет работой САД и формулирует задания для модуля [Moses] — прувера САД.

В качестве альтернативного прувера вы можете использовать SPASS, эффективный резолюционный прувер в логике первого порядка с равенством. SPASS разработан в Max Plank Institute for Informatics, в Саарбрюкене, Германия.