|
Архив публикацийТезисыXX-ая конференцияАппликативный подход при автоматическом доказательстве теоремКИФФ, Россия, 121151, Москва, Кутузовский пр. 24/1, +74957291442, allo10@yandex.ru 1 стр. (принято к публикации)Как известно, за 50 лет развития автоматического доказательства теорем и логического вывода устоялись две основных системы: - система опровержения на основе резолюций; - система дедукций на основе правил (прямая, обратная или смешанная). Появились достаточно точные правила преобразования высказываний на языке Исчисления Предикатов Первого Порядка (ИППП) в так называемую Конъюнктивную Нормальную Форму (КНФ). Для вышеуказанных целей используется символьная обработка в КНФ дизъюнктов и логических связок с подстановкой и унификацией значений переменных различными программными средствами на базе традиционной архитектуры Фон-Неймана. Что представляется не очень удобным, так как в процессе вычислений не применяется ни одна арифметическая операция. При аппликативном подходе в автоматическом доказательстве теорем и логическом выводе процесс доказательства представляется в избранном комбинаторном базисе и сводится к системе продукций с набором правил и достаточно простой системой управления с возможностью добавления комбинаторных выражений для эвристических и весовых функций с аппаратной поддержкой комбинаторного базиса. В результате не тратится программно-аппаратный ресурс на выполнение элементарной операции (аппликации). Комбинаторы базиса возможно представить в двоичном коде в виде битовой строки. Это позволяет использовать существующую в настоящее время программно-аппаратную вычислительную среду, построенную на двоичной арифметике. Существенным отличием аппликативного подхода является активное участие в процессе автоматического доказательства логических связок, представленных в комбинаторном виде. Практически, в любом языке программирования мы можем определить одной командой вычисление логического значения применения логической связки только к двум логическим аргументам. При аппликативном подходе логические связки выражены в том же комбинаторном базисе, что и аргументы и количество логических связок и аргументов может быть более двух, что приводит к унификации логических операций и существенному повышению производительности вычислений. |