Правила вывода в исчислении предикатов (силлогизмы)

Лекция 4 Правила вывода в исчислении предикатов (силлогизмы) Семантика исчисления предикатов обеспечивает основу для формализации теории ло­гического вывода. Возможность логически выводить новые правиль­ные выражения из набора истинных утверждений - это важное свойство исчисления предикатов. Логически выведенные выражения корректны, потому что они совместимы со всеми предыдущими интерпретациями первоначального набора выражений. Говорят, что интерпретация, которая делает предложение истинным, удовлетво­ряет этому предложению. Если интерпретация удовлетворяет каждому элементу на­бора выражений, то говорят, что она удовлетворяет набору. Выражение X логически следует из набора выражений S исчисления предикатов, если каждая интерпретация, которая удовлетворяет S, удовлетворяет и X. Это утверждение дает основание для проверки правильности правил вывода: функция логического вывода должна произ­водить новые предложения, которые логически следуют из данного набора предло­жений исчисления предикатов. Важно верно понимать значение слов логически следует: логическое следование вы­ражения X из S означает, что оно должно быть истинным для каждой интерпретации, ко­торая удовлетворяет первоначальному набору выражений S. Оно должно быть истинным и при любой другой интерпретации, которую мог бы иметь этот набор выражений. Термин логически следует вовсе не означает, что X выведено из S, или что его можно вывести из S. Это просто означает, что X истинно для каждой интерпретации, которая удовлетворяет S. Однако системы предикатов могут иметь бесконечное число возможных интерпретаций, поэтому практическая необ­ходимость проверять все интерпретации возникает весьма редко. В вычислительном от­ношении правила вывода позволяют определять, когда выражение как компонент интерпретации логически следует из этой интерпретации. Логическое следование Пусть даны формулы A1,… , Am, B. Формула B является логическим следствием формул A1,… ,Am, если, придавая значения переменным X1,… ,Xn , от которых зависят все рассматриваемые формулы, всякий раз, когда истинны одновременно все формулы A1,… , Am, истинна и формула B. Для логического следствия используется запись A1,… , Am => B Для проверки логического следования достаточно построить истинностную таблицу. Пример Проверить что X, Y, (ZXY) => Z Используем для проверки таблицу истинности: X Y Z ZXY Z T T T F F T T F T T Из второй строки видно, что представленное выражение есть логическое следствие. Понятие логически следует обеспечивает формальное основание для доказательства разумности и правильности правил вывода. Правило вывода обеспечивает создание новых предложений исчисления предикатов на основе данных предложений. Следовательно, правила вывода производят новые пред­ложения, основанные на синтаксической форме данных логических утверждений. Если каждое предложение X, полученное с помощью некоторого правила вывода на множест­ве S логических выражений, также логически следует из S, то говорят, что это правило вывода обосновано. Если система правил вывода способна произвести каждое выражение, которое может логически следовать из S, то говорят, что эта система правил вывода является полной. Определение Удовлетворять, модель, адекватность Интерпретация I удовлетворяет выражению X, если она истинна при некотором выборе переменных, от которых зависит X. Интерпретация I называется моделью для совокупности формул A1,… , Am, если они истинны в I I => A1,… , Am X выполнимо тогда и только тогда, когда существуют такая интерпретация и значение переменной, которые ему удовлетворяют; в противном случае X невыпол­нимо. Набор выражений выполним тогда и только тогда, когда существуют интерпретация и значения переменных, которые удовлетворяют каждому элементу. Если набор выражений невыполним, то говорят, что он противоречив. Если выражение X истинно в любой интерпретаций, то говорят, что X адекватно. Выражение X (p(X)p(X)) противоречиво, потому что оно не может быть удов­летворено ни при какой интерпретации или значениях переменных. С другой стороны, выражение X (p(X)p(X)) адекватно. Для проверки адекватности выражений, не содержащих переменных, можно исполь­зовать метод таблиц истинности. Поскольку не всегда можно определить, адекватно ли выражение, содержащее переменные, говорят, что полное исчисление предикатов "неразрешимо". Однако существуют методы доказательства, которые позволяют генерировать любое выражение, логически следующее из данного набора выражений. Они называются процедурами полного дока­зательства. Определение Процедура доказательства — это комбинация правил вывода и ал­горитма применения этих правил к набору логических выражений для создания но­вых предложений. Определение Логически следует, обоснованный и полный Выражение исчисления предикатов X логически следует из набора S выражений ис­числения предикатов, если каждая интерпретация и значения переменных, которые удовлетворяет S, удовлетворяют и X. Правило вывода обосновано, если каждое выражение исчисления предикатов, полученное в соответствии с правилом из множества S выражений исчисления пре­дикатов, также логически следует из S. Правило вывода полно, если на данном множестве S выражений исчисления предикатов правило позволяет вывести любое выражение, которое логически следует из S. Правило modus ponens (правило отделения, или модус поненс) - это обоснованное правило вывода. Если дано выражение вида PQ и другое выражение вида Р, и оба вы­ражения истинны на интерпретации I, то modus ponens позволяет нам сделать вывод, что Q тоже истинно на этой интерпретации. Действительно, поскольку modus ponens яв­ляется обоснованным правилом, Q истинно для всех интерпретаций, для которых P и PQ являются истинными. Определение Модус поненс, модус толленс, исключение «И», введение «И», универсальное инстанцирование Если известно, что предложения P и PQ истинны, то модус поненс позволяет вы­вести Q. Согласно правилу вывода модус толленс (modus tollens), если известно, что PQ яв­ляется истинным и Q ложно, можно вывести Р. Исключение "И" - правило, позволяющее вывести истинность обоих конъюнктов на основе истинности конъюнктивного предложения. Например, если PQ истинно, можно сделать вывод, что P и Q истинны. Введение "И" позволяет вывести истинность конъюнкции из истинности ее конъюнк­тов. Например, если P и Q истинны, то конъюнкция PQ истинна. Универсальное инстанцирование сводится к следующему: если любую переменную, стоящую под квантором всеобщности в истинном предложении, заменить любым со­ответствующим термом из области определения, то результирующее выражение — истинно. Таким образом, если a принадлежит той же области определения, что и X и X p(X), то можно вывести p(а). В качестве простого примера применения правила модус поненс в исчислении выска­зываний рассмотрим следующие предложения: "если идет дождь, то земля будет влаж­ной" и "идет дождь". Если P обозначает "идет дождь" и Q есть "земля, влажная", то пер­вое выражение можно записать в виде PQ. Поскольку действительно сейчас идет дождь (P истинно), получаем систему аксиом. PQ P Применив правило модус поненс к набору истинных выражений, можно добавить тот факт, что земля является влажной Q. Правило модус поненс также может быть применено к выражениям, содержащим переменные. Рассмотрите в качестве примера обычный силлогизм "все люди смерт­ны, и Сократ — человек, поэтому Сократ — смертен". Высказывание "Все люди смертны" может быть представлено в исчислении предикатов так. X (человек(Х)смертный(Х)). человек(сократ). Поскольку X в выражении стоит под знаком квантора всеобщности, его можно заме­нить любым значением из области определения X, и при этом утверждение будет сохра­нять истинное значение согласно правилу универсального инстанцирования. Заменив в выражении X на сократ, получим следующее утверждение. человек(сократ) смертный(сократ). Применив правило модус поненс, приходим к выводу смертный(сократ). Он может быть добавлен к набору выражений, которые логически следуют из первоначаль­ных утверждений. Можно использовать так называемый алгоритм унификации для определения автоматическим решающим устройством правомочности замены X на сократ и возможности применения правила модус поненс Унификация Чтобы применять правила вывода типа модус поненс, система вывода должна уметь определять, когда два выражения являются эквивалентными, или равносиль­ными. В исчислении высказываний это тривиально: два выражения равносильны то­гда и только тогда, когда они синтаксически идентичны. В исчислении предикатов определение равносильности двух предложений усложняется наличием переменных. Правило универсального инстанцирования позволяет заменять переменные под зна­ком квантора всеобщности термами из области определения. Необходимо определить процесс замены переменных, при котором несколько выражений могут стать идентичными (обычно для того, чтобы можно было применять правила вывода). Унификация — это алгоритм определения необходимых подстановок с целью приве­дения в соответствие двух выражений исчисления предикатов. Пример такого процесса приведен ранее, где терм сократ из выражения человек(сократ) был использован в качестве подстановки для X в выражении X(человек(X)=>смертный(X)). Эта подстановка позволила применить правило модус поненс и получить вывод смертный(сократ). Унификация и такие правила вывода, как модус поненс, позволяют делать выводы на множестве логических утверждений. Для этого логическая база данных должна быть вы­ражена в соответствующей форме. Весьма важный аспект этой формы заключается в требовании, чтобы все переменные стояли под знаком квантора всеобщности. Это обеспечивает полную свободу в выполне­нии подстановок. Переменные, стоящие под квантором существования, можно устранить из предложений в базе данных, заменив их константами, обеспечивающими истинность предложения. Например, Х parent(X, tom) может быть заменено выражением parent(bob, tom) или parent(mary, tom), принимая во внимание, что Боб (bob) и Мэри (mary) являются родителями Тома (tom) в этой интерпретации. Процесс удаления переменных, связанных квантором существования, усложнен тем фактом, что значение этих подстановок может зависеть от значения других переменных в выражении. Например, в высказывании X Y mother(X,Y) значение переменной Y под квантором существования зависит от значения X. Сколемизация - это замена каждой переменной, связанной квантором существования, функцией несколь­ких или всех имеющихся в предложении переменных, которая возвращает соответст­вующую константу. В вышеупомянутом примере, поскольку значение Y зависит от X, Y можно заменить сколемовской функцией f от X. Это порождает предикат X mother(X, f(X)). Сколемизация - это процесс, который также позволяет связывать переменные, стоящие под квантором всеобщности, с константами. После удаления из логической базы данных переменных, связанных квантором суще­ствования, можно применить унификацию и привести предложения в форму, необходи­мую для применения таких правил вывода, как модус поненс. Процесс унификации осложняется тем фактом, что переменная может быть заменена любым термом, включая другие переменные и функциональные выражения произволь­ной сложности. Эти выражения могут тоже содержать переменные. Например, father(jack) можно использовать в качестве подстановки для X в выражении man(Х) для получения вывода, что отец Джека смертен. Приведем несколько реализаций выражения foo(X,a,goo(Y)). Их можно получить путем следующих подстановок. foo(fred,a,goo(Z)) foo(W,a, goo(jack)) foo(Z,a,goo(moo(Z))) В этом примере экземпляры подстановки, или унификации, которые делают началь­ное выражение идентичным каждому из трех, можно записать в виде {fred/X, Z/Y} {W/X, jack/Y} {Z/X, moo(Z)/Y} Запись X/Y, ... означает, что X является подстановкой для переменной Y в первоначальном выражении. Подстановка также называется связыванием. Говорят, что перемен­ная связана со значением, используемым в качестве подстановки. При создании алгоритма унификации, который вычисляет подстановки, необходимые для соответствия двух выражений, возникают некоторые проблемы. Хотя константу можно систематически использовать в качестве подстановки для пе­ременной, любая константа рассматривается как "базовый экземпляр" и не может быть заменена. Нельзя также два различных "базовых экземпляра" использовать в качестве подстановки для одной и той же переменной. Переменная не может быть унифицирована с термом, содержащим ее. Поэтому пере­менная X не может быть заменена на р(Х), поскольку это порождает бесконечное выра­жение: р(р(р(р(...Х)...). Тест для этой ситуации называется проверкой вхождения. Вообще, процесс решения задачи требует ряда выводов и, следовательно, ряда последова­тельных унификаций. Логические решающие устройства задач должны поддерживать согла­сованность подстановок для переменных. Важно, чтобы любая унифицирующая подстановка была сделана согласованно по всем вхождениям этой переменной во все выражения. А выра­жения должны быть приведены в соответствие друг другу. Эта ситуация уже встречалась, ко­гда терм сократ использовался не только в качестве подстановки для переменной X в предложении человек(Х), но и для переменной X в выражении смертен(Х). Если переменная связана, все последующие унификации и процедуры вывода должны учитывать это. Если переменная связана с константой, ее уже нельзя связы­вать с другим термом при последующих унификациях. Если переменная X1 использо­валась в качестве подстановки для другой переменной Х2, а затем была заменена константой, то в Х2 тоже необходимо отразить это связывание. Множество замен, ис­пользуемых в последовательности выводов, играет важную роль, потому что оно может содержать ответ на первоначальный вопрос. Например, ес­ли p(а, Х) унифицировать с предпосылкой правила p(Y, Z)=>q(Y, Z) при помощи под­становки {a/Y, X/Z}, модус поненс позволяет вывести q(a, X) при той же подстанов­ке. Если мы сопоставим этот результат с предпосылкой правила q(W, b)=>r(W, b), то выведем r(a,b) с учетом множества подстановок {a/W, b/X}. Другое важное понятие - это композиция подстановок унификации. Если S и S' яв­ляются двумя множествами подстановок, то композиция S и S' (пишется SS') получается после применения S' к элементам S и добавления результата к S. Рассмотрим пример композиции последовательности подстановок {X/Y, W/Z}, {V/X), {a/V, f{b)/W}. Они эквивалентны единственной подстановке {a/Y, f(b)/Z}. Эта подстановка была выведена путем компоновки {X/Y, W/Z} с {V/Х} для полу­чения {V/Y, W/Z} и компоновки результата с {a/V, f(b)/W} для получения {a/Y, f(b)/Z}. Композиция подстановок - это метод, с помощью которого объединяются подста­новки унификации. Можно показать, что композиция является ассоциативной, но не коммутативной. Последнее требование алгоритма унификации - унификатор должен быть максимально общим, т.е. для любых двух выражений должен быть найден наиболее общий унификатор. Это очень важно, поскольку при потере общности в процессе решения уменьшается вероятность достижения окончательного решения или такая возможность исчезает полностью. Например, предложения p(Х) и p(Y) можно унифицировать любым константным вы­ражением вида {fred/X, fred/Y}. Однако fred не является наиболее общим унификато­ром. Используя в качестве унификатора любую переменную, можно получить более об­щее выражение: {Z/X, Z/Y}. Решения, полученные при использовании первой подста­новки, всегда будут ограничены содержащейся в них константой fred, лимитирующей логические выводы. Следовательно, fred можно использовать в качестве унификатора, но это снижает универсальность результата. Определение Наиболее общий унификатор Если s - произвольный унификатор выражения E, а g - наиболее общий унифика­тор этого набора выражений, то в случае применения s к E будет существовать еще один унификатор s' такой, что Es=Egs', где Es и Egs' — композиции унификаций, примененные к выражению Е. Наиболее общий унификатор для набора выражений определяется с точностью до обозначения. В конечном счете, не имеет никакого значения, как называется перемен­ная - X или Y, поскольку это не снижает общности для результирующей унификации. Унификация важна для любой системы решения задач искусственного интеллекта, использующей в качестве средства представления исчисление предикатов. Унифика­ция определяет условия, при которых два (или больше) выражения исчисления преди­катов могут быть эквивалентными.