Проблема дедукции (в ИВ и ИП).

Пусть имеется множество формул S = {H₁, H₂, …, H_n }, а также еще одна формула С. Говорят, что С является логическим следствием множества S (S╞ C), если при любой интерпретации, при которой все Н_i истинны, С также истинна. При этом формулы H_i называются гипотезами. Проблема дедукции – это исследование того, является ли произвольно заданная формула С логическим следствием заданного множества гипотез S.

 

Утверждение.  Для того, чтобы S╞ C, н. и д., чтобы формула F = H₁ Ù H₂ Ù … Ù H_n É C была общезначимой.

Воспользуемся эквивалентным преобразованием для исключения импликации:

F1 º ù(H₁ Ù H₂ Ù … Ù H_n) Ú C º ùH₁ Ú ùH₂ Ú … Ú H_n Ú C = F2.

 

Решение проблемы дедукции методом обратной дедукции – это доказательство (или опровержение) того, что F2 – общезначима.

 

Рассмотрим F3 = ùF2. Для того, чтобы S╞ C, н. и д., чтобы F3 была невыполнимой.

 

F3 º ù(ùH₁ Ú ùH₂ Ú … Ú ùH_n Ú C) º H₁ Ù H₂ Ù … Ù H_n Ù ùC = F4.

 

Решение проблемы дедукции методом обратной дедукции – это доказательство (или опровержение) того, что F4 – невыполнима.

 

Определение 1.1. Пусть два дизъюнкта C₁ и C₂ имеют следующий вид: C₁=AÚX, C₂=BÚ ùY, где A и B — некоторые дизъюнкты, а X и Y — атомарные формулы такие, что X=Y.

Тогда дизъюнкт (C₁\X) È (C₂\ ùY) является резольвентой дизъюнктов C₁ и C₂.

Определение 1.2. Логическим выводом дизъюнкта C из множества дизъюнктов S назовем такую последовательность дизъюнктов C₁,C₂,...,C_n, что C_iÎS или C_i является резольвентой некоторых C_j и C_k, j<i, k<i, 1< i £ n, и C_n=C.

В системах искусственного интеллекта понятие логического вывода и выводимости тесно связаны с принципом дедукции и резолюционным выводом пустого дизъюнкта L.

Определение 1.3. Будем говорить, что целевой дизъюнкт (цель) C выводим (доказуем) в множестве гипотез S={H₁,...,H_m}, если в S существует опровержение С, то есть логический вывод пустого дизъюнкта L из расширенного множества дизъюнктов SÚ ùC={H₁,...,H_m, ùC}: C₁,C₂,...,C_n, C₁= ùC, C_n= L.

Для того, чтобы различать вывод цели в смысле определения 1.3 и вывод как последовательность резольвент в смысле определения 1.2, последний будем называть резолюционным выводом непустого дизъюнкта.

Рассмотрим подробнее понятие хорновских дизъюнктов и взаимосвязь последних с базами знаний.

Определение 1.4. Хорновским называется такой дизъюнкт, который содержит не более одной позитивной литеры. Хорновский дизъюнкт называется точным, если он содержит позитивную литеру. В противном случае он называется негативным.

Частным случаем точного дизъюнкта является унитарный позитивный дизъюнкт, сводящийся к одиночной позитивной литере. Если дизъюнкт представлен одиночной позитивной литерой, не содержащий переменных, то такой дизъюнкт называется элементарным.

В системах искусственного интеллекта точный дизъюнкт выражает некоторое правило: негативные литеры соответствуют посылкам (которые представлены соответствующими высказываниями), а позитивная литера представляет заключение. Унитарный позитивный дизъюнкт представляет некоторый факт, то есть заключение, не зависящее ни от каких посылок. Задача состоит в том, чтобы проверить, является ли некая формула, называемая целью, логически выводимой из множества фактов и правил. В этом случае используется метод резолюций, являющийся методом доказательства от противного. Исходя из фактов, правил и отрицания цели, представленного негативным хорновским дизъюнктом, метод резолюций пытается прийти к противоречию — пустому дизъюнкту L.

Без ограничения общности можно рассматривать лишь такие хорновские дизъюнкты, все литеры которых различны. Таким образом, каждый дизъюнкт множества гипотез, расширенного отрицанием цели (расширенного множества), будет иметь один из трех следующих видов:

1) p, положительная литера; либо

2) pÚ ùq₁Ú ùq₂Ú...Ú ùq_n, где n≥1 и q₁, q₂,..., q_n — различные литеры, p —литера; либо

3) ùq₁Ú ùq₂Ú...Úùq_m, где m≥1 и q₁, q₂,..., q_m — различные литеры.

Из рассмотрения можно исключить также тавтологии, то есть для дизъюнктов вида pÚùq₁Úùq₂Ú...Úùq_n дополнительно потребовать, чтобы литера p не совпадала ни с одной из литер q₁, q₂,..., q_n.

Классическим механизмом логического вывода является метод резолюций, предложенный Дж.Робинсоном в 1965 году и опирающийся на принцип дедукции. Общая идея метода состоит в следующем: чтобы получить некоторое заключение С, исходя из гипотез H₁,H₂,...,H_n, то есть проверить, является ли C логическим следствием гипотез H₁,H₂,...,H_n, достаточно проверить, является ли противоречивой формула H₁ÙH₂Ù...ÙH_nÙùC, в которой отрицание заключения добавлено к исходным гипотезам. При этом рассматриваются лишь формулы стандартного вида — КНФ. Тогда полученная формула может быть интерпретирована как множество дизъюнктов S={H₁,H₂,...,H_n,ùC}, доказательство невыполнимости которого эквивалентно построению в нем логического вывода пустого дизъюнкта.

Таким образом, невыполнимость множества S можно проверить, порождая логические следствия из него до тех пор, пока не будет получен пустой дизъюнкт L. Для порождения логических следствий используется правило резолюции:

{AÚX,BÚ ù X} ╞ AÚB, где A, B, X —формулы.

В силу неразрешимости логики предикатов первого порядка для выполнимого множества дизъюнктов S процедура, основанная на принципе резолюций, может работать бесконечно долго.

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

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

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

В семантической резолюции используется интерпретация для разделения множества дизъюнктов S на два класса: S₁ — непустое множество дизъюнктов, которое выполняется (т.е. принимает значение «истина») некоторой интерпретацией, S₂ — непустое множество дизъюнктов, которое не выполняется (т.е. принимает значение «ложь») этой интерпретацией; S₁ÈS₂=S. Разрешается резольвирование дизъюнктов, принадлежащих только разным множествам, и запрещается образование резольвент от дизъюнктов, входящих в одно и то же множество. Тем самым сокращается образование ненужных дизъюнктов, так как только резольвированием из разных множеств можно получить пустой дизъюнкт.

Другим способом ограничения количества порождаемых дизъюнктов является упорядочение предикатных букв. Если имеется упорядочение предикатных букв типа P₁>P₂>...>P_k, то разрешается резольвирование литеры, обладающей наибольшим порядком, то есть P₁.

В семантической резолюции допускается любая интерпретация и любое упорядочение предикатных букв. Семантическая резолюция полна.

Идея лок-резолюции состоит в использовании индексов для упорядочения литер в дизъюнктах из множества дизъюнктов S. Иными словами, она включает индексацию произвольным образом каждого вхождения литеры в S некоторым целым числом; разные вхождения одной и той же литеры в S могут быть индексированы по-разному. После этого резольвировать разрешается только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставится в соответствие наименьший из этих индексов.

Лок-резолюция полна и является весьма эффективным методом логического вывода. Основным недостатком лок-резолюции является то, что она несовместима с большинством других стратегий, даже таких естественных, как, например, со стратегией избегания противоречивых дизъюнктов. Кроме того, совершенно неясно, как по данному множеству дизъюнктов a priori установить, какая из начальных индексаций литер дает более эффективную лок-резолюцию.

Линейная резолюция. Линейным выводом из множества дизъюнктов S называется последовательность дизъюнктов C₁,C₂,...,C_n, в которой верхний дизъюнкт С₁ÎS, а каждый член C_i+1, i=1,2,...,n-1, является резольвентой дизъюнкта C_i, называемого центральным, и дизъюнкта B_i, называемого боковым. При этом B_i должен удовлетворять одному из следующих двух условий:

1) либо B_iÎS, i=1,2,...,n-1,

2) либо B_i является некоторым дизъюнктом C_j, предшествующим в выводе дизъюнкту C_i, то есть j<i. Таким образом, линейный вывод начинается с некоторого дизъюнкта, применяет к нему правило резолюции для получения резольвенты, затем применяет резолюцию к этой резольвенте и некоторому дизъюнкту, и так далее, пока не будет получен пустой дизъюнкт.

Линейная резолюция может быть дополнительно усилена введением понятия упорядоченного дизъюнкта и использованием информации о резольвированных литерах. В таком виде она называется OL-выводом и является разновидностью линейной резолюции с функцией выбора (SL-вывод)

Линейная резолюция и OL-вывод полны. Линейная резолюция является одной из наиболее эффективных стратегий. Особую привлекательность линейному выводу придает его простая структура. Кроме того, линейная резолюция совместима со стратегией множества поддержки, вместе с ней удобно применять эвристические методы.

Все рассмотренные выше стратегии эффективнее общего метода резолюций, однако, остаются переборными.

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

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

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

Единичная резолюция — это линейная резолюция, в которой по крайней мере одна из посылок — единичный дизъюнкт. Использование единичной резолюции приводит к тому, что на каждом этапе некая литера удаляется из одного дизъюнкта. Поэтому алгоритм проверки невыполнимости конечных множеств хорновских дизъюнктов ИВ с помощью линейной единичной резолюции имеет сложность N² , где N — число литер, первоначально присутствующих в S с учетом повторений. Поскольку единичная и входная линейная резолюции эквивалентны, для последней справедлива та же оценка. Сейчас существует линейный по времени алгоритм проверки невыполнимости множеств хорновских дизъюнктов ИВ.

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

Для получения полиномиальной оценки по времени необходимо введение дополнительных ограничений на КНФ и хорновские формулы ИП. Так, для ИП предложен полиномиальный (квадратичный по времени) алгоритм для баз знаний, описываемых хорновскими формулами с одноместными предикатами. Существенные ограничения накладываются также на использование функций. Предлагался частный случай семантической резолюции, эффективный для сингулярных баз знаний, т.е. описываемых одноместными предикатами и функциями. Однако накладываемые в этих случаях ограничения на базы знаний на практике неприемлемы, поскольку, в то время как любой m‑арный предикат может быть представлен в виде произведения бинарных, требование одноместности предикатов базы знаний существенно снижает выразительную способность логической модели.

Методом, альтернативным резолюции, является обратный дедуктивный метод Маслова. Он сформулирован для аксиоматических систем, но может быть также применен и для логических исчислений. В этом методе поиск вывода идет от целевой формулы к аксиомам или постулатам, истинность которых априорно известна. Чтобы определить выводимость формулы C из посылок H₁,H₂,...,H_n, необходимо найти формулы-предшественники, из которых C может быть выведена одним применением правила вывода. Затем по каждой из полученных формул-предшественников, не являющейся аксиомой исчисления, в свою очередь определяется множество непосредственных формул-предшественников и так далее, вплоть до построения окончательного вывода.

На основе обратного метода вывода были разработаны и реализованы машинный алгоритм вывода и алгоритм машинного поиска логического вывода в ИВ, носившие экспериментальный характер, было показано что метод может быть также распространен на весьма широкие классы дедуктивных систем.

Для стандартизированных формул метода резолюций оба метода примерно эквивалентны. Кроме того, идеи стратегий и доказательств их полноты обычно равноприемлемы для метода резолюций и обратного метода.

Поскольку задача разрешимости логического выражения, приведенного к КНФ, для ИП является NP-полной, общая оценка этих методов совпадает с оценкой для метода резолюций. Однако для некоторых частных случаев их применение может приводить к существенному ускорению вывода.

Резолюционные и связанные с ними методы весьма интересны, так как являются систематическими и могут быть реализованы на ЭВМ. Однако ввиду алгоритмической неразрешимости ИП невозможно определить эффективную стратегию решения для всех областей приложения. Кроме того, эффективность логических программ резко падает с увеличением числа предложений. Поэтому на практике добиваются устранения причин «комбинаторного взрыва» числа резолюций, имеющего место при доказательстве теорем практической степени сложности, за счет использования семантики и встраивания в правила вывода и алгоритмы унификации специфики конкретной области применения.

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

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

· Использование естественного параллелизма методов логического вывода, подразумевающее разработку параллельных реализаций Пролога и соответствующих аппаратных средств. Эта идея легла в основу проекта создания ЭВМ пятого поколения с принципиально новой, параллельной архитектурой;

· Разработка новых эффективных универсальных методов решения логических задач, поиск методов и средств ускорения логического вывода.

 

 

 Рассмотрим пример логического вывода.

 

 S =

{ 1) P(a,b); 2) P(b,c); 3) (P(x,y), ù P(a,z), ù P((b,u)); 4) (P(x,y), ù P(b,y))}

C = P(a,c).

 

Присоединим отрицание цели к множеству гипотез:

 

1) P(a,b);                                                4) (P(x,y), ù P(b,y));

2) P(b,c);                                                5) ù P(a,c). 

3)) (P(x,y), ù P(a,z), ù P((b,u));

 

Необходимо помнить, что резолюционные методы в ИП содержат две основные процедуры: унификацию и резолюцию.

 

Рассмотрим логические выводы, построенные двумя методами: единичной резолюцией и входной линейной резолюцией. 

 

МЕТОДЫ ПОВЫШЕНИЯ ЭФФЕКТИВНОСТИ ЛОГИЧЕСКОГО ВЫВОДА.