С помощью логики предикатов

Представление знаний и получение выводов

Лекция.5.

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

2.5.1.Основные понятия логики предикатов.

Логика может быть использована для описания высказываний, отношений между высказываниями и правил вывода одних высказываний из других.

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

В исчислении предикатов объекты представляются в виде термов. Различают термы трёх типов: константа, переменная, составной терм. Константа - это символ, обозначающий индивидуальный объект или понятие. Переменная - это символ, используемый в разное время для обозначения разных индивидуальных объектов. Переменные вводятся лишь одновременно с кванторами. Составной терм состоит из функционального символа и упорядоченного множества термов, являющихся его аргументами. Функциональный символ описывает характер зависимости. То есть составной терм обозначает объект, зависящий от других объектов, представленных его аргументами.

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

В логике предикатов выделяют два класса символов.

Логические связки - это символы первого класса. Они позволяют определить новые составные предикаты, используя введённые. К символам первого класса относятся:

1) ~ А отрицание (не А)

2) А /\ В конъюнкция (А и В)

3) А \/ В дизъюнкция (А или В)

4) А -> В импликация (А влечёт В)

5) А <-> В эквивалентно (А эквивалентно В)

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

С = ~ А - истинно, если А - ложно и ложно, если А истинно;

С = А /\ В - истинно, тогда и только тогда, когда А и В одновременно истинны;

С = А \/ В - истинно, тогда и только тогда, когда истинны А или В;

С = А -> В - истинно, если А - ложно или одновременно А и В истинны.

Замечание: В естественном языке: если А и В истинны, то С - истинно; а если А - ложно, то С не определено. В логике это доопределяется.

С = А <-> В - истинно, если А и В вместе истинны, либо А и В - ложны.

Логические связки 4) и 5) сводятся к основным связкам в соответствии со следующими формулами:

A -> B <=> (~A) \/ B (2.5.1)

A <-> B <=> (A -> B) /\ (B -> A) (2.5.2)

A <-> B <=> (~A \/ B) /\ (~B \/ A) (2.5.3)

Символы второго класса (кванторы) - это символы, которые вводят ограничения на переменные. Различают квантор общности-", и квантор существования - $. Они определяются следующим образом:

("X) F(X) - F истинно для всех значений X;

($X) F(X) - существует такое X, для которого F – истинно.

Переменная, которая проквантирована называется связной. Ниже представлены примеры использования кванторов.

Примеры:

1) Высказывание “какое бы X не взяли, если X - синица, то X - птица ” запишется следующим образом

("X) синица (X) -> птица (X);

2) Высказывание “существует Z, что Z-студент и Z-имеет стипендию = 500” запишется следующим образом

($Z) студент (Z) /\ имеет стипендию (Z, 500).

Логические символы упорядочены по силе следующим образом:

первая группа: $,", ~;

вторая группа: \/, /\;

третья группа: ->, <->.

2.5.2. Приведение логических формул к стандартной форме.

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

Процесс приведения формулы исчисления предикатов к стандартной форме состоит из шести этапов.

Этап 1. Исключение импликаций и эквивалентностей в соответствии с формулами (2.5.1 - 2.5.3). Например, если формула имеет вид

" (X) (синица (X) -> птица (X)),

то она преобразуется к следующему виду

" (X) (~синица (X) \/ птица (X)).

Этап 2. Перенос отрицания внутрь формулы. На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. При этом используются следующие формулы:

~(A /\ B) <=> (~A) \/ (~B) (2.5.4)

~(A \/ B) <=> (~A) /\ (~B) (2.5.5)

~(("X) A(X)) <=> ($X (~A(X))) (2.5.6)

~(($X) A(X)) <=> ("X (~A(X))) (2.5.7)

После завершения этого этапа каждое вхождение отрицания в формулу будет относиться лишь к атомарным подформулам. Например, формула вида

~(птица (синица) /\ существующая (синица))

преобразуется в формулу вида

~птица (синица) \/ ~существующая (синица);

а формула с переменными вида

~(("X) птица (X))

преобразуется в формулу вида

($X) (~птица(X)).

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

Правило 1. Если переменная, связанная квантором существования, является крайней слева, то такую формулу можно заменить функцией без аргументов, т.е. константой.

Правило 2. Приоритетность действия кванторов определяется в порядке слева направо. Переменной, которая влияет на связанную квантором существования переменную, является любая переменная с квантором общности, которая среди всех упорядоченных символов стоит левее этой переменной.

Например, формула вида

($X)(студент(X) /\ имеет стипендию(X,500))

преобразуется в формулу вида

студент(g1) /\ имеет стипендию (g1,500), где g1- сколемовская константа.

Если формула содержит кванторы общности, то процедура усложняется. Например, высказывание “для любого X существует такое Y, что X любит Y” запишется с помощью формулы следующим образом

("X)($Y)(любит (X,Y))

и будет преобразована в формулу вида

("X)(любит (X, f(X))).

Это означает, что если выделить конкретное X, то для него существует конкретное Y, т.е. Y определяется в зависимости от X или Y=f(X). При подстановке этой функции на место переменной Y данный факт будет отражён и сам квантор не потребуется. Функция f(X) называется сколемовской функцией.

Этап 4. Вынесение кванторов общности в начало формулы и их исключение. Например, формула вида

("X)(синица(X)\/воробей(X))/\("Y)(волк(Y)\/медведь(Y))

преобразуется в формулу вида

("X)("Y)(синица(X)\/воробей(X))/\(волк(Y)\/медведь(Y)),

а затем преобразуется в формулу

(синица(X)\/воробей(X))/\(волк(Y)\/медведь(Y)).

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

Этап 5. Использование дистрибутивных законов для конъюнкции и дизъюнкции. На этом этапе формула преобразуется к специальному виду - конъюнктивной нормальной форме (КНФ). КНФ – это последовательность элементов, соединённых конъюнкциями, где каждый элемент является либо литералом, либо литералами, соединёнными символом дизъюнкции \/. Под литералом понимают атомарный предикат либо отрицание атомарного предиката. Для преобразований на этом этапе используются следующие тождества:

(A /\ B) \/ C = (A \/ C) /\ (B \/ C) (2.5.8)

A \/ (B /\ C) = (A \/ B) /\ (A \/ C) (2.5.9)

Например, формула вида

выходной(X)\/(учится(Y,X)/\усталый(Y))

преобразуется в формулу вида

(выходной(X)\/учится(Y,X))/\(выходной(X)\/усталый(Y)),

что на естественном языке формулируется следующим образом: для любого X, во-первых, X – выходной день, либо студент Y учится в день X; во-вторых, X – выходной день, либо студент Y усталый.

Этап 6. Выделение множества дизъюнктов. Формула, полученная к этапу 6 - это совокупность конъюнктивных членов, являющихся литералами либо литералами соединёнными дизъюнкцией. На данном этапе не важно знать структуру вложенности. Если доказана истинность каждого литерала, то не важно в каком порядке их группировать. Например, формула вида

(A/\В)/\(С/\(D/\E))

преобразуется в формулу вида

A /\ B /\ C /\ D /\ E.

Порядок литералов также не важен. То есть, если A и B истинно, то и B и A истинно. Таким образом, отбросив символ /\ можно записать литералы в виде совокупности {A,B,C,D,E}. Каждый литерал в общем случае является дизъюнктом. Например, литерал A можно представить в виде

((W \/Y)\/Z) \/ (B\/X), где переменные W,Y,Z,B,X - литералы. Аналогично, отбросив символ \/ литералы можно переписать в виде совокупности: {W,Y,Z,B, X}.

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

(выходной(X)\/учится(Y,X))

и дизъюнкт 2

(выходной(X)\/усталый(Y)).

Рассмотрим пример, демонстрирующий все этапы. Имеется высказывание “если все люди относятся с почтением к некоторому человеку, то этот человек -король”. С помощью формулы оно запишется следующим образом

("X)("Y) (человек(Y) -> почитает(Y,X) -> король(X)).

На первом этапе, используя формулу (2.5.1), получаем следующую формулу

("Х)(~(("Y)(~человек(Y)\/почитает(Y,X)))\/король(Х).

На втором этапе, используя формулу (2.5.5), получаем следующую формулу

("Х)($Y)(человек(Y)/\~почитает(Y,X))\/король (Х).

На третьем этапе, используя правило 2, получаем следующую формулу

("Х)(человек(f1(X))/\~почитает(f1(X),X))\/король(Х).

На четвёртом этапе исключаем квантор общности и получаем следующую формулу

(человек(f1(X))/\~почитает(f1(X),Х))\/король (Х).

На пятом этапе, используя формулу (2.5.8), получаем формулу

(человек(f1(X))\/король (Х))/\(~почитает(f1(X),Х)\/король(X)).

На шестом этапе из формулы выделяем следующие дизъюнкты:

(человек(f1(X)) \/король (Х)) (состоит из двух литералов);

(~почитает(f1(X),Х) \/ король (Х)) (состоит из двух литералов).

2.5.3. Принцип резолюции и доказательство теорем.

Когда имеется совокупность высказываний в стандартной форме, то интересно исследовать к каким следствиям они приводят. Высказывания, которые исходно считаются истинными – это аксиомы или гипотезы. Высказывания, следующие из них – это теоремы. Резолюция - это правило вывода, говорящее о том, как одно высказывание может быть получено из других. Принцип резолюции был предложен в 60-х годах Робинсоном и применялся для автоматического доказательства теорем. Главная идея правила резолюции состоит в следующем: “Если одна и та же атомарная формула появляется как в левой части одного дизъюнкта, так и в правой части другого дизъюнкта, то дизъюнкт, получаемый в результате соединения этих двух дизъюнктов, из которых вычеркнута повторяющаяся формула, является следствием указанных дизъюнктов.”

Введем следующую форму записи дизъюнктов: записываются сначала литералы без отрицания, а затем литералы с отрицанием. Эти две группы будем разделять знаком группой символов ":- ". Литералы без отрицания будем отделять друг от друга символом ";". Литералы с отрицанием запишем без символа ~, разделяя их запятыми. Таким образом, дизъюнкт в общем виде будет иметь вид:

A;B;...:- K,L,...,

где A,B,…- литералы без отрицания, а K,L,… - литералы с отрицанием.

Такая запись имеет мнемонический смысл, поскольку:

формула (A \/ B \/...) \/ (~K \/ ~L \/...) равносильна

формула (A \/ B \/...) \/ ~(K /\ L /\...) равносильна

формула (K /\ L /\...) -> (A \/ B \/...).

Например, формула

человек(адам)/\человек(ева)/\(человек(Х)\/~мать(X,Y)\/~человек(Y))

запишется в виде: человек(адам):-.

человек(ева):-.

человек(X):-мать(X,Y),человек(Y).

А это выглядит в точности как определение на Прологе объекта "человек".

Предположим имеются высказывания, представленные в виде следующих логических формул без переменных:

зеленеет(трава),поют(птицы):-наступила(весна);

греет(солнце),увеличился(день):-зеленеет(трава).

Применяя принцип резолюции получим следующую формулу:

поют(птицы),греет(солнце),увеличился(день):-наступила(весна).

В том случае, если высказывания представлены в виде логических формул с переменными, принцип резолюции формулируется следующим образом:”Если имеются два дизъюнкта, представленные в виде структур, и выполняется сопоставление соответствующих подструктур, то результат соединения этих структур и является представлением нового дизъюнкта (возможно сопоставление нескольких литералов).” Процедура "сопоставления" называется унификацией. Поясним действие принципа резолюции на примере. Используя результаты заключительного примера раздела 2.5.2, высказывание “если каждый человек почитает кого-то, то этот кто-то король” запишется с помощью формул следующим образом:

человек(f1(X));король(Х):-. (2.5.10)

король(Y):-почитает(f1(Y),Y). (2.5.11)

Высказывание “каждый человек почитает Артура” запишется с фомощью формулы

почитает(Z, артур):-человек(Z). (2.5.12)

Применяя принцип резолюции к формулам (2.5.11) и (2.5.12) получаем

король (артур):-человек(f1(артур)). (2.5.13)

Применяя принцип резолюции к (2.5.10) и (2.5.13) получаем

король(артур);король(артур):-.

То есть, истинно высказывание ”Артур является королем”.

Существует два способа использования метода резолюций для доказательства утверждений.

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

Второй способ устраняет недостаток первого способа. Если имеется множество гипотез, то к нему добавляются дизъюнкты, соответствующие отрицанию высказывания, которое надо доказать. Резолюция даст пустой дизъюнкт в точности тогда, когда доказываемое высказывание следует из данных гипотез. Пустой дизъюнкт - логическое выражение ложности. Описанный метод отражает свойство полноты метода резолюции.

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

Добавим ко множеству дизъюнктов (2.5.10)-(2.5.12) целевой дизъюнкт (дизъюнкт для проверки на совместимость с дизъюнктом король(артур))

:-король(артур). (2.5.14)

Применяя метод резолюции получим пустой дизъюнкт

:-.

То есть, дизъюнкт ~король(артур) не совместим с указанными гипотезами. Следовательно, высказывание “Артур является королем” следует из данных гипотез.

2.5.4. Представление знаний с помощью

логики предикатов – основа языка Пролог.

Для представления знаний в языке Пролог были выбраны дизъюнкты специального вида – хорновские дизъюнкты (ХД). Хорновский дизъюнкт - это дизъюнкт, содержащий не более одного литерала без отрицания. Существует два вида ХД:

1)ХД, содержащий один литерал без отрицания;

2)ХД, не содержащий таких литералов.

Каждая разрешимая задача с помощью ХД представляется в следующем виде. Имеется только один дизъюнкт без заголовка (ХД вида 2). Все остальные дизъюнкты имеют заголовки (ХД вида 1). ХД вида 2 описывают цель. ХД вида 1 описывают гипотезу.

Формулы Пролога - это есть не что иное, как ХД. Утверждения в Прологе - ХД с заголовком. Целевой дизъюнкт в Прологе - ХД без заголовка. Целевой дизъюнкт в Прологе - ХД без заголовка. Пролог-система основывается на процедуре доказательства теорем методом резолюций для ХД. Конкретная стратегия, используемая при этом является разновидностью линейной входной резолюции.

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

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

:-мать(джон,Х), мать(X,Y).

и утверждения

мать(U,V):-родитель(U,V),женщина(V).

Получаем результат

:-родитель(джон,Х), женщина(Х), мать(X,Y).

Здесь произошло сопоставление целевого утверждения и утверждения с подходящим заголовком. При этом, переменная U конкретизируется значением “джон”.

Все описанное выше относится к событиям, происходящим после того, как Пролог выбрал утверждение для сопоставления с первой целью. Каким образом организуется исследование альтернативных утверждений для удовлетворения той же самой цели? В Прологе используется стратегия поиска вглубь, а не поиска вширь. Такая стратегия намного проще и требует меньших затрат памяти при реализации на ЭВМ. Программы на Прологе похожи на гипотезы о проблемной области, а вопросы похожи на теоремы, которые необходимо доказать.

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

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

Дата добавления: 2014-01-07