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

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

- дочь короля и королевы – принцесса.

- принцесса может почувствовать горошину.

Удалим квантор существования из предложений C1, C2, обозначив через f1, f2 сколемовские функции без переменных, так как перед квантором существования нет квантора общности.

: f1 – мужчина.

f2 – женщина.

Опускаем кванторы всеобщности в C3, C4. Проводим резолюцию C1 с C3, а затем C2 и C4. Получаем:

f1 – король или простолюдин.

f2 – королева или простолюдинка.

Затем осуществляем парамодуляцию C7 и C5. Это дает:

дочь королевы и f1 – есть принцесса или f1 - простолюдин. Затем осуществляем парамодуляцию C8 и C9. Это дает:

дочь f1 и f2 есть принцесса, либо f1, либо f2 – простолюдин. Наконец парамодуляция C10 с C6 дает:

дочь f1 и f2 может почувствовать горошину, либо f1, либо f2 – простолюдин.

4.2.4 Стратегии очищения

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

4.2.4.1 Стратегия предпочтения одночленов

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

4.2.4.2 Факторизация

Размер предложений по длине можно уменьшить, используя подстановки, так что некоторые литералы в предложении становятся одинаковыми. Эта операция называется факторизацией. Например:

C = {A(x, f(k)), A(b, y), A(a, f(x)), A(x, z)}

можно факторизовать подстановкой:

=(b/x, f(k)/y, f(b)/z).

Тогда получим:

C = {A(b, f(k)), A(a, f(b)), A(b, f(b))}.

C называется факториалом предложения C. Фактор предложения не обязательно единственный. Другой фактор:

= (a/x, f(k)/y, f(a)/z),

C = {A(a, f(k)), A(b, f(k)), A(a, f(a)}.

4.2.4.3 Использование подслучаев

Для любой пары предложений C, D S предложение C называется подслучаем предложения D, если существует такая подстановка , что C D. Например:

C = {A(x)},

D = {A(b), P(x)},

то подстановка

= (b/x)

приведет к

C = {A(b)}.

то означает сокращение литералов.

4.2.4.4 Гиперрезолюция

Можно делать так, чтобы в резолюции участвовали сразу по несколько предложений. Это называется гиперрезолюцией. Предположим, что для конечного множества предложений {C1, …, Cn} и единственного предложения B удовлетворяются следующие условия:

1. B содержит n литералов L1, …, Ln.

2. Для каждого i, 1 i n, предложение Ci, содержит литерал , но не содержит дополнений никакого другого литерала из B и никакого литерала из любого предложения Cj, j i.

Множество Sa = {Ci} {B} будем называть конфликтом, а предложение:

его гиперрезольвентой. Ra можно вывести из Sa.

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

В качестве примера гиперрезолюции рассмотрим множества:

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

Sa - конфликт с резольвентой , и Sa – скрытый конфликт.

4.2.4.5С – упорядочение

С – упорядочение предполагает линейность, так как при его определении различаются левое и правое родительские предложения. Пусть С – предложение из S. Обозначим через [C] предложение C с заданным на нем произвольным порядком литералов, а через [S] – множество таких упорядоченных предложений. Если предложение [C] порождается в линейном выводе то пусть [C^i-1] и [B^i-1] будут его левым и правым предложениями с литералами предложения C^i-1, расположенными в порядке (где т.е. самый правый литерал левого родительского выражения является литералом резолюции), и с литералами предложения B^i-1 в порядке . Ясно, что для некоторого i (i =1m). Тогда упорядоченное предложение Cⁱ таково:

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

Пример:

Компьютерный практикум

Реализовать алгоритм C – упорядочивания.

119

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

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