Формально-графическая интерпретация логического вывода

Аннотация

В статье рассматриваются суживающие (сокращающие перебор) стратегии для резолюционных алгоритмов логического вывода в базах знаний, построенных на основе логической модели знаний. Особенностью этих стратегий является предварительная настройка на работу с конкретными базами знаний. Для настройки используется метод абстракций и формально-грамматическая интерпретация логического вывода. Абстракция – это функция, которая отображает класс задач K1 в более простой класс K2. При решении задачи A принадлежит K1 ее отображают в задачу B принадлежит K2. Затем задача B решается, и ее решения используются для поиска решений исходной задачи A. В настоящей работе класс задач K1 – это проблема дедукции в исчислении предикатов первого порядка. Для K1 рассматриваются две абстракции – пропозициональная, при которой K2 – это проблема дедукции в исчислении высказываний, и абстракция, при которой проблема дедукции решается для конструкций, названных псевдо-предикатами. Для обеих абстракций предлагается формально-грамматическая интерпретация, позволяющая выполнить предварительную настройку, которая гарантирует перебор лишь успешных вариантов выводов. Приведенные примеры иллюстрируют достоинства предложенной методики.