47524 (597342), страница 7

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 7)

В данном случае L(x) и не находятся в дополнительном отношении. При подстановке a вместо x будут получены, соответственно, и , и поскольку эти предикаты отличаются только символами отрицания, то они находятся в дополнительном отношении. Однако, операцию подстановки нельзя проводить при отсутствии каких-либо ограничений.

Подстановку t в x принято записывать как {t/x}. Поскольку в одной ППФ может находиться более одной переменной, можно оказаться необходимо провести более одной подстановки. Обычно эти подстановки записываются в виде упорядоченных пар {t1/x1, …, tn/xn}.

Условия, допускающие подстановку:

• xi – является переменной,

• ti – терм (константа, переменная, символ, функция) отличный от xi,

• для любой пары элементов из группы подстановок, например (ti/xi и tj/xj) в правых чачтях символов / не содержится одинаковых переменных.

Унификация

Обозначим группу подстановок {t1/x1, …, tn/xn} через . Когда для некоторого представления L применяется подстановка содержащихся в ней переменных {x1, …, xn}, то результат подстановки, при которой переменные заменяются соответствующими им термами t1, …, tn принято обозначать L.

Если имеется группа различных выражений на основе предиката L, то есть L1, …, Lm}, то подстановка , такая, что в результате все эти выражения становятся одинаковыми, то есть L1 = L2 = … = Lm, - называется унификатором {L1, …, Lm}. Если подобная подстановка существует, то говорят, что множество {L1, …, Lm} унифицируемо.

Множества {L(x), L(a)} унифицируемо, при этом унификатором является подстановка (a/x).

Для одной группы выражений унификатор не обязательно единственный. Для группы выражений {L(x, y), L(z, f(x)} подстановка = {x/z, f(x)/y} является унификатором, но является также унификатором и подстановка = {a/x, a/z, f(a)/y}. Здесь a – константа, x – переменная. В таких случаях возникает проблема, какую подстановку лучше выбирать в качестве унификатора.

Операцию подстановки можно провести не за один раз, а разделив ее на несколько этапов. Ее можно разделить по группам переменных, проведя, например, подстановку {t1/x1, t2/x2, t3/x3, t4/x4} сначала для {t1/x1, t2/x2}, а затем для {t3/x3, t4/x4}. Допустимо также подстановку вида a/x разбить на две подстановки u/x и a/u. Результат последовательного выполнения двух подстановок и также подстановка и обозначается .

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

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

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

Положим, что при просмотре последовательно всех выражений в порядке слева направо несовпадающими термами оказались x, t. Например, получено {L(a, t, f(z)), L(a, x, z)}. В этом случае, если:

1. x является переменной;

2. x не содержится в t, к группе подстановок добавляется {t/x}.

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

В приведенном примере третий терм в одном случае z, а в другом – f(z), первое условие выполняется, а второе – нарушается. Поэтому подстановка недопустима. Если в группе предикатных выражений остается хотя бы одно такое, для которого никакими подстановками нельзя получить совпадения с другими выражениями, такая группа называется неунифицируемой.

Рассмотрим другой пример:

P1 = L(a, x, f(g(y))),

P2 = L(z, f(z), f(u)).

1. Первые несовпадающие члены: {a, z}.

Подстановка: a/z. Имеем:

P1 = L(a, x, f(g(y))),

P2 = L(a, f(a), f(u)).

1. Первые несовпадающие элементы {x, f(a)}. Подстановка: [f(a)/x]. Имеем:

P1 = L(a, f(a), f(g(y))),

P2 = L(a, f(a), f(u)).

1. Первые несовпадающие элементы {g(y), u}. Подстановка: [g(y)/u]. Получаем совпадение. Следовательно, НОУ: [a/z, f(a)/x, g(y)/u].

Алгоритм доказательства

Пусть заданы:

Предикаты делаются дополнительными с помощью подстановки [a/x]. Суждение о том, становятся ли два выражения дополнительными, выносится:

1. По различию используемых символов.

2. По существованию НОУ для двух выражений, в которых удалены одинаковые символы.

Далее все делается рекуррентно.

Пример 1. Милиция разыскивает всех въехавших в страну, за исключением дипломатов. Шпион въехал в страну. Однако, распознать шпиона может только шпион. Дипломат не является шпионом.

Оценим вывод: среди милиционеров есть шпион.

Воспользуемся следующими предикатами:

Въехал(x): x въехал в страну.

Дипломат(x): x – дипломат.

Поиск(x, y): x разыскивает y.

Милиционер(x): x – милиционер.

Шпион(x): x – шпион.

Если выразим через эти предикаты посылку и вывод в форме ППФ, то получим:

для всех x, если x не является дипломатом, но въехал в страну, найдется милиционер y, который его разыскивает.

Если существует шпион x, который въехал в страну, и некоторый y разыскивает его, то он сам шпион.

Для всех x справедливо, что если x является шпионом, то он не дипломат.

Заключение:

Существует x такой, что он является шпионом и милиционером.

Если эти формулы преобразовать в клаузальную нормальную форму, то получим:

Заключение преобразуем в свое отрицание:

и затем в клаузальную форму без квантора общности.

Последующий процесс доказательства имеет вид:

дипломат(а)милиционер(f(а)) [a/x] из 2,4 (9)

милиционер(f(а)) [a/x] из 8,9 (10)

дипломат(а)поиск(f(а),а) [a/x] из 1,4 (11)

поиск(f(а),а) [a/x] из 8,11 (12)

шпион(f(a)) [a/x] из 12,5 (13)

[f(a)/x)] из 10 и 14 (15)

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

4.2.3.3 Задачи, использующие равенства

Новые предложения получались до сих пор двумя способами: подстановкой и резолюцией. При резолюции пары предложений, отображаются в новые предложения, а подстановка заменяет терм в предложении другим термом той же синтаксической формы. Иногда возникает необходимость заменить терм равным ему термом, который не является термом, для которого возможна подстановка (подстановочным случаем) в первом терме. Рассмотрим простой пример. Положим f(x, y) = x + y. При сравнении предложений:

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

1. Работать с предложениями, в которых равенство выражено в виде атомов.

2. Быть операцией, превращающей два предложения в третье.

Это специальное правило вывода называется парамодуляцией.

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

Правило парамодуляции

Если для заданных предложений C1 и C2 = (’ = ’, B) (или C2’ = (’ = ’, B)), не имеющих общих переменных в общей части B выполняются условия:

1. C1 содержит терм .

2. У и ’ есть наиболее общий унификатор:

,

где ui и wj – переменные соответственно из ’ и ,

то надо построить предложения =C11, а затем C#, заменяя ’ на ’2 для какого-то одного вхождения ’ в C₁^*. Наконец вывести:

C3=(C#, B).

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

C1={Q(a)},

C2={a=b}

можно вывести:

C3={Q(b)}.

Несколько более сложный случай:

C1={Q(x)},

C2={(a=b)}.

Подстановка = (a/x) дает:

C1^*={Q(a)},

C3={Q(b)}.

При одном применении парамодуляции подстановка =2 применяется в С₁^* только один раз. Таким образом, если заданы предложения:

C1={Q(x), P(x)},

C2={(a=b)},

то одно применение парамодуляции с подстановкой = (a/x) дает сначала

C₁^*={Q(a), P(a)},

а затем или

C3={Q(a),P(b)},

либо

C3={Q(b), P(a)}.

Для получения C4={Q(b), P(b)} требуется повторное применение парамодуляции.

Рассмотрим пример по сюжету известной сказки Андерсона «Принцесса на горошине», который может служить тестом на наличие королевской крови.

Определения для примера:

1. x, y, z – переменные, принимающие значения на множестве людей.

2. M(x): x – мужчина.

3. C(x): x – простолюдин.

4. D(x): x может почувствовать горошину через перину.

5. x = k: x – король.

6. x = q: x – королева.

7. d(x,y): дочь x и y.

8. x = p: x – принцесса.

Исходные предложения:

- существует мужчина.

- существует женщина.

- любой мужчина не простолюдин король.

- любая королева – женщина и не простолюдинка.

Характеристики

Список файлов книги