В данном документе описывается процесс разработки оболочки для интерактивных систем вывода пустого дизъюнкта на основе метода резолюций. Для простоты изложения рассмотрим метод резолюций применительно к пропозициональной логике. Данный метод позволяет дать ответ на вопрос, является ли анализируемая
формула пропозициональной логики F тавтологией, путем построения на ее основе вывода пустого дизъюнкта □. Для этого необходимо рассмотреть отрицание этой формулы ¬F и показать, что ¬F является противоречием (тождественно-ложной формулой). Перед построением вывода при помощи эквивалентных преобразований (исключение импликации, применение законов де Моргана и дистрибутивности и т.п.) пропозициональная формула ¬F преобразуется в эквивалентную ей конъюнктивную нормальную форму (КНФ) вида
¬F = D1 ˄ … ˄ Dn. Каждый дизъюнкт Di(i=1, …, n) представляет собой дизъюнкцию литералов Di = L1 ˅ … ˅ Lk. Каждый литерал Lj(j = 1, …,k) имеет вид p или ¬p, где p обозначает некоторую пропозициональную переменную. На основе полученного представления ¬F в КНФ формируется множество дизъюнктов Ω, которое изначально имеет вид Ω = {D1,…,Dn}. Далее начинается процесс вывода пустого дизъюнкта □, в котором на каждом шаге выполняются следующие действия.
1. В множестве дизъюнктов Ω ищется резольвируемая пара, т.е. пара вида (D'˅ p, D''˅p). Поскольку таких пар в Ω может быть много, то, чтобы не решать задачу перебора, выбор пары делается в интерактивном режиме.
2. К резольвируемой паре применяется правило резолюции (D' ˅ p), (D''˅¬p) ⇒ (D'˅ D''). Результат применения правила – резольвента есть новый дизъюнкт Dn+1=D' ˅ D''.
3. Если полученная резольвента есть пустой дизъюнкт (Dn+1= □), то вывод считается законченным, а пропозициональная формула F является тавтологией. В противном случае Dn+1добавляется в Ω и выполняется переход к п.1.
Если на некотором шаге вывода в Ω невозможно добавить ни одной новой резольвенты, то формула F не является тавтологией.
Разрабатываемая оболочка состоит из специализированного редактора «Редактор базы пропозициональных формул», управляемого расширенной графовой грамматикой языка пропозициональной логики, и решателя задач, агенты которого реализуют алгоритм вывода пустого дизъюнкта, формируя при этом соответствующий граф вывода.
Орграф грамматики (метаинформации), описывающий абстрактный синтаксис языка пропозициональной логики, представлен на рис. 1. Орграф информации, описывающий грамматику языка текстового представления (конкретный синтаксис) пропозициональных формул, представлен на рис. 2.
Рис. 1. Орграф грамматики языка пропозициональной логики
Рис. 2. Орграф информации, описывающий грамматику языка текстового представления пропозициональных формул
Спецификатор дуги «непустой список» имеет символьное обозначение «*», а ограничитель дуги «создание нового или ссылка на существующее понятие» – «ref-new». Здесь и далее символ «@» в метках вершин, представленных пунктирными прямоугольниками, разделяет метку корневой вершины стороннего орграфа и метку той его вершины (не совпадающей с первой), которая является корневой вершиной повторно используемого подграфа. В квадратных скобках у вершин указаны метки соответствующих им вершин из орграфа грамматики (метаинформации). Орграф информации, представляющий таблицу соответствий для орграфа грамматики языка пропозициональной логики, показан на рис. 3.
Рис. 3. Таблица соответствий для орграфа грамматики языка пропозициональной логики
Специализированный редактор «Редактор базы пропозициональных формул» создается путем подключения к инструментальному средству платформы IACPaaS «Редактор орграфов информации» расширенной графовой грамматики языка пропозициональной логики в качестве информации, управляющей процессом редактирования и генерацией интерфейса.
Орграф грамматики (метаинформации), описывающий абстрактный синтаксис языка представления графов вывода пустого дизъюнкта на основе метода резолюций, показан на рис. 4. Спецификатор дуги «ноль или один» имеет символьное обозначение «[!]».
Рис. 4. Орграф грамматики языка представления графов вывода пустого дизъюнкта на основе метода резолюций
Орграф информации, представляющий таблицу соответствий для орграфа грамматики, описывающий абстрактный синтаксис языка представления графов вывода пустого дизъюнкта методом резолюций, изображен на рис. 5.
Рис. 5. Таблица соответствий для орграфа грамматики языка представления графов вывода пустого дизъюнкта на основе метода резолюций
На рис. 6 показан интерфейс инструментального средства платформы «Редактор решателей задач», с помощью которого, сформирована декларативная спецификация решателя задач «Решатель задач оболочки интерактивных систем вывода пустого дизъюнкта на основе метода резолюций». Отметим, что в собственных информационных ресурсах на чтение указано две таблицы соответствий. Это связано с тем, что орграф грамматики, описывающий абстрактный синтаксис языка представления графов вывода пустого дизъюнкта на основе метода резолюций, имеет ссылку на подграф орграфа грамматики языка пропозициональной логики. С последним связана таблица соответствий, используемая агентом «Интерфейсный контроллер расширяемых редакторов и просмотрщиков информационных единиц» для обращения к модулю «АИСТ» (анализ и синтез текстов), который формирует текстовое представление пропозициональных формул на основе, указанной в таблице соответствий грамматики.
Рис. 6. Интерфейс инструментального средства «Редактор решателей задач», в котором сформирована декларативная спецификация решателя задач
Таблица соответствий для орграфа грамматики языка представления графов вывода пустого дизъюнкта методом резолюций используется агентом «Интерфейсный контроллер расширяемых редакторов и просмотрщиков информационных единиц» для обращения к агентам «Агент Сформировать множество дизъюнктов» и «Агент Применить правило резолюций» (путем посылки сообщений, сформированных по специальным шаблонам). Обращение к агенту «Агент Сформировать множество дизъюнктов» выполняется при создании вершины, соответствующей вершине «Множество дизъюнктов» из орграфа грамматики. Данный агент применяет к отрицанию выбранной пользователем пропозициональной формулы набор эквивалентных преобразований с целью получения ее представления в КНФ. Затем формирует начальное множество дизъюнктов, создавая в графе вывода пустого дизъюнкта вершину «Множество дизъюнктов» и делая ее прямыми потомками корневые вершины подграфов, представляющих пропозициональные формулы, являющиеся дизъюнктами в полученной КНФ. Обращение к агенту «Агент Применить правило резолюций» выполняется при создании вершины, соответствующей вершине «Резольвента» из орграфа грамматики. Данный агент применяет правило резолюции к выбранной пользователем на очередном шаге вывода резольвируемой паре пропозициональных формул (дизъюнктов). Если пара не задана, то агент отображает сообщение об этом. В противном случае он создает в графе вывода пустого дизъюнкта вершину «Резольвента». Затем, если резольвируемая пара представляет собой пару только контрарных литералов, то у вершины «Резольвента» потомков не создается, вывод считается завершенным. В противном случае делает прямым потомком вершины «Резольвента» и вершины «Множество дизъюнктов» корневую вершину подграфа, представляющего полученную в результате применения правила пропозициональную формулу (дизъюнкт), расширяя таким образом множество дизъюнктов.
Содержимое стартовой web-страницы «Интерактивная система вывода пустого дизъюнкта на основе метода резолюций» решателя задач «Решатель задач оболочки интерактивных систем вывода пустого дизъюнкта на основе метода резолюций» выглядит следующим образом.
На рис. 7 продемонстрирован пример работы сервиса «Сервис вывода пустого дизъюнкта методом резолюций в пропозициональной логике», созданного с использованием разработанной оболочки. База пропозициональных формул сформирована с помощью специализированного редактора оболочки «Редактор базы пропозициональных формул». Выходным фактическим параметром здесь является орграф информации, представляющий базу графов вывода пустого дизъюнкта методом резолюций.
Рис.7. Интерфейс сервиса «Сервис вывода пустого дизъюнкта методом резолюций в пропозициональной логике»
Все подграфы, корневые вершины которых соответствуют вершине «Пропозициональная формула» в орграфе грамматики языка пропозициональной логики, отображаются в текстовом представлении. Однако при нажатии на кнопку-иконку « 
» у некоторой вершины, соответствующей вершине «Пропозициональная формула», отображение подграфа этой формулы заменяется с текстового представления на структурное. На рис. 8 показано структурное представление пропозициональной формулы, соответствующей третьему дизъюнкту ¬a ˅¬b в множестве дизъюнктов. При нажатии на кнопку-иконку « 
» данная формула вновь будет отображена в текстовом представлении.
Рис.8. Фрагмент интерфейса сервиса «Сервис вывода пустого дизъюнкта методом резолюций в пропозициональной логике». Дизъюнкт ¬a˅ ¬bв структурном представлении