English
!

Архив публикаций

Тезисы

XX-ая конференция

Аппликативный подход при автоматическом доказательстве теорем

Мажирин И.В.

КИФФ, Россия, 121151, Москва, Кутузовский пр. 24/1, +74957291442, allo10@yandex.ru

1  стр. (принято к публикации)

Как известно, за 50 лет развития автоматического доказательства теорем и логического вывода устоялись две основных системы:

- система опровержения на основе резолюций;

- система дедукций на основе правил (прямая, обратная или смешанная).

Появились достаточно точные правила преобразования высказываний на языке Исчисления Предикатов Первого Порядка (ИППП) в так называемую Конъюнктивную Нормальную Форму (КНФ). Для вышеуказанных целей используется символьная обработка в КНФ дизъюнктов и логических связок с подстановкой и унификацией значений переменных различными программными средствами на базе традиционной архитектуры Фон-Неймана. Что представляется не очень удобным, так как в процессе вычислений не применяется ни одна арифметическая операция.

При аппликативном подходе в автоматическом доказательстве теорем и логическом выводе процесс доказательства представляется в избранном комбинаторном базисе и сводится к системе продукций с набором правил и достаточно простой системой управления с возможностью добавления комбинаторных выражений для эвристических и весовых функций с аппаратной поддержкой комбинаторного базиса. В результате не тратится программно-аппаратный ресурс на выполнение элементарной операции (аппликации). Комбинаторы базиса возможно представить в двоичном коде в виде битовой строки. Это позволяет использовать существующую в настоящее время программно-аппаратную вычислительную среду, построенную на двоичной арифметике.

Существенным отличием аппликативного подхода является активное участие в процессе автоматического доказательства логических связок, представленных в комбинаторном виде. Практически, в любом языке программирования мы можем определить одной командой вычисление логического значения применения логической связки только к двум логическим аргументам. При аппликативном подходе логические связки выражены в том же комбинаторном базисе, что и аргументы и количество логических связок и аргументов может быть более двух, что приводит к унификации логических операций и существенному повышению производительности вычислений.



© 2004 Дизайн Лицея Информационных технологий №1533