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

Размещено на http://www.allbest.ru/

Лекция

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

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

Говорят, что интерпретация, которая делает предложение истинным, удовлетворяет этому предложению. Если интерпретация удовлетворяет каждому элементу набора выражений, то говорят, что она удовлетворяет набору. Выражение 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, полученное с помощью некоторого правила вывода на множестве 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, поскольку это не снижает общности для результирующей унификации.

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

предикат квантор разумность подстановка

Размещено на Allbest.ru