| ||||||||
|---|---|---|---|---|---|---|---|---|
| ||||||||
Система Автоматизации Дедукции (САД) разрабатывается в рамках исследований по Алгоритму Очевидности. Система предназначена для автоматической обработки формальных математических текстов, записанных в языке ForTheL (FORmal THEory Language). Также допускается ввод в языке первого порядка. Подробные сведения о входных языках САД вы можете получить на странице Пояснения, из примеров секвенций, теорем и текстов, а также из Руководства по языку ForTheL (на английском языке, gzipped PS или PDF). Система САД распространяется бесплатно с открытым исходным кодом по лицензии GNU GPL. Вы можете загрузить её в виде пакета исходного кода либо пакета исходного кода вместе с исполнимыми файлами (Linux i386) на странице Загрузить. По приведенным ниже гиперссылкам вы можете получить доступ к системе САД в режиме онлайн. Введите ForTheL-текст или секвенцию, предназначенную к обработке, установите параметры поиска вывода и запустите САД. Система обработает задание и вернет результат: перевод ForTheL-текста, дерево доказательства или протокол верификации. Текущая версия системы выполняет следующие задания:
Каждая строка в результирующем выводе "подписана" одним из модулей САД. Модули [ForTheL] и [FOL] отвечают за синтаксический анализ языка ForTheL и первого порядка, соответственно. Модуль [TPTP] обрабатывает задания и наборы аксиом в формате TPTP. Модуль [Reason] управляет работой САД и формулирует задания для модуля [Moses] — прувера САД.
В качестве альтернативного прувера вы можете использовать
SPASS,
эффективный резолюционный прувер в логике первого порядка
с равенством. SPASS разработан в
Max Plank Institute
for Informatics, в Саарбрюкене, Германия.
В распространяемом пакете САД настроен также для работы с пруверами
Vampire,
E prover,
Prover9
и Otter.
К системе несложно подключить любой прувер, использующий стандартный
формат входного задания, такой как TPTP или DFG. | ||||||||
|
