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

(4) Отец(Александр, Сергей),

(5) Отец(Сергей, Ричард).

(6) Отец(Сергей, Иван).

Сначала неаксиоматически зададим процедуру, которая из логических формул выводит заключение. Вывод формулы C из логических формул A, B будем задавать в виде схемы:



А: Все люди смертны

В: Сократ - человек

С: Сократ - смертен.

Если в переменную подставляется значение, то слева от наклонной черты запишем имя переменной, а справа - значение. Например, если в переменную x подставляется значение Сократ, то будем это записывать как x/Сократ.

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

Например, предположим, что задан вопрос: «Кто дедушка Ричарда?». Его можно записать в виде:

(x)(дедушка(x, Ричарда)).

Ответ может быть получен в следующей последовательности:



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

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

В логике предикатов такая процедура полностью формализована и носит название метода резолюции.

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

4.2.2 Процесс нормализации

4.2.2.1Префиксная нормальная форма

Рассмотрим фразу «любой человек имеет отца». Ее можно представить в логике предикатов в следующем виде:

(x)(человек(x) (y)(отец(y, x))).

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

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

Во-первых, необходимо исключить связки и . По определению:

Следовательно, во всех комбинациях ППФ можно ограничиться тремя связками , и .

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

Легко показать:

1.

Это соответствует: высказывание не имеет отношения к квантору переменной, которая включена в другой предикат.

Между предикатами существует следующее соотношение:

Таким образом, «необязательно F(x) выполняется для всех x» «существует такое x, что F(x) не выполняется»; «не существует такое x, что выполняется F(x)» «для всех x не выполняется F(x)».

Далее имеем:

2.(x)F(x)(x)H(x) = (x)(F(x)H(x))

(x)F(x)(x)H(x) = (x)(F(x)H(x)).

Это означает, что квантор обладает дистрибутивностью относительно , а - относительно .

С другой стороны:

(x)F(x)(x)H(x)(x)(F(x)H(x)).

(x)F(x)(x)H(x)(x)(F(x)H(x)).

Это легко показать. Пусть для первого выражения x определен на множестве D ={а, б, в}, при этом истиной являются F(а), F(б), H(в). Тогда левая часть не выполняется, а правая истинна. На самом деле справедливо:

(x)F(x)(x)H(x)(x)(F(x)H(x)).

(x)F(x)(x)H(x)(x)(F(x)H(x)).

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

(x)F(x)(x)H(x) = (x)F(x) (y)H(y),

(x)F(x) (x)H(x) = (x)F(x) (y)H(y).

Теперь H(y) не содержит переменной x и поэтому не зависит от связывания x. Отсюда:

3. (x)F(x)(x)H(x) = (x)(y)(F(x) H(y)),

(x)F(x) (x)H(x) = (x)(y)(F(x) H(y)).

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

1. Используя формулы для , , заменим их на , , .

2. Воспользовавшись выражениями

внесем отрицания внутрь предикатов.

3. Вводятся новые переменные, где это необходимо.

4. Используя 1, 2, 3 получаем префиксную нормальную форму.

В качестве примера рассмотрим следующее выражение:

Шаг1:

Шаг2:

Шаг 3: нет необходимости.

Шаг 4: используем выражение 1 по переменной z -

Теперь применяем выражение 1 по переменной w -

4.2.2.2 Скалемовская нормальная форма

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

Это означает, что если выделить конкретное x, то для этого x существует y, удовлетворяющее функции подсистема(x, y). Иными словами, y зависит от x, то есть, если задано x, то и существует соответствующее ему y. Отсюда следует, что y можно заменить на функцию f(x), которая задает отношение между x и y. Поскольку f(x) возникло из-за того, что переменная y квантифицирована , при подстановке функции на место y, квантор уже не требуется. Таким образом, исходную логическую формулу можно переписать: (x) подсистема(x, f(x).

Такая функция называется скалемовской.

Приоритетность действия кванторов, имеющихся в префиксной форме, определяется слева направо. Например: (x)(y)(z)F(x, y, z) (x)(z)F(x, f(x), z). А для случая: (x)(z)(y)F(x, y, z) (x)(z)F(x, f(x, y), z).

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

(x)(y)подсистема(x, y) =подсистема.

Если проделать эту операцию для примера, получим:

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

(x)(y)(z)(w)F(x ,y ,z, w) = (x)(z)F(x, f(x), z, g(x, z)).

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



Такое представление и есть сколемовская нормальная форма.

Теперь можем определить алгоритм получения сколемовской формы:

1. Составить список L переменных, связанных квантором общности. Сначала список L пуст.

2. Пусть C_i - рассматриваемое предложение, j - номер использующейся сколемовской функции S_ij. Положим j = 1.

3. Удалить кванторы , начиная с самого левого и применяя в зависимости от необходимости правила а или б.

а. Если рассматривается квантор x, то удалить его и добавить x к списку L.

б. Если рассматривается квантор x, то удалить его и заменить x во всем предложении C_i термом S_ij(x1, …, xk), где x1, …, xk переменные, находящиеся в этот момент в списке L. Увеличить j на 1.

Следующим шагом является переход к конъюнктивной нормальной форме, а затем к клаузальной форме, то есть форме предложений.

Приведение к конъюнктивной нормальной форме осуществляется заменой пока это возможно (AB)C на (AC)(BC). В результате получим выражения вида A1 … An, где Ai имеет вид (, причем есть терм или атомарный предикат или атомарная формула или их отрицание. Целесообразно осуществить и минимизацию по следующим правилам:

Наконец, исключаем связку , заменяя AB на две формулы A, B. В результате многократной замены получим множество формул, каждая из которых является предложением. Это и есть клаузальная нормальная форма.

4.2.2.3 Предложения Хорна

Все клаузальные формулы (предложения) представляют собой несколько предикатов, то есть:

Эти формулы в зависимости от k, l классифицируются по нескольким типам.

(1) Тип 1: k = 0, l = 1.

Предложение представляет собой единичный предикат, и оно может быть записано как F(t1, t2, …, tm), где t1, t2, …, tm - термы. В случае когда все термы представляют собой константы, они описывают факты, которые соответствуют данным из БД. Если термы содержат переменные, то они задают общезначимые представления, высказываемые для группы фактов. Например, таким представлением является:

текучесть(x): все течет, все изменяется.

(2) Тип 2: k1, l = 0.

Этот тип можно записать в виде:

F1F2…Fk.

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

(3) Тип : k1, l=1.

Этот тип соответствует записи в форме «Если ___, то ____.».

F1F2…FkG1.

(4) Тип: k=0, l>1.

Этот тип имеет вид:

G1G2…Gl

и используется при представлении информации, содержащей нечеткость. Обычно нечеткость возникает при неполноте информации. В этой формуле появляется неполнота информации в том смысле, что из нее нельзя определить, какой из предикатов G1, …, Gl является истиной.

(5) Тип: k1, l>1.

Это наиболее общий тип.

В системе предложений Хорна среди всех перечисленных типов предложений допустимы типы предложений 1, 2, 3, а 4, 5 запрещены.

4.2.3Формализация процесса доказательств

Доказательство демонстрирует, что некоторая ППФ является теоремой на заданном множестве аксиом (то есть результатом логического вывода из аксиом).

Положим, что есть множество из n ППФ, а именно, A1, A2, …, An, и пусть ППФ, для которой требуется вычислить является ли она теоремой, есть B. В таких случаях можно сказать, что доказательство показывает истинность ППФ вида:

(A1…AnB) (1)

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

(2)

не выполняется (ложно) при любой интерпретации.

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

Основная идея метода, называемого методом резолюции, состоит:

1. В проверке содержит или не содержит S пустое предложение.

2. В проверке выводится или не выводится пустое предложение из S, если пустое предложение в S отсутствует.

Любое предложение C_i, из которого образуется S, является совокупностью атомарных предикатов или их отрицаний (предикат и его отрицание называются литералами), соединенных символами дизъюнкции, вида:

Сама же S является конъюнктивной формой, то есть имеет вид:



Следовательно, условием истинности S является условие истинности всех C_i в совокупности.

Условием ложности S является ложность по крайней мере одного C_i. Однако, условием, что C_i будет ложным в какой-нибудь интерпретации, является то, что множество будет пустым. Это легко показать. Положим, что это не так, тогда среди всех возможных интерпретаций имеется такая, что какой-нибудь из литералов этого множества или все они будут истиной и тогда C_i не будет ложью. Следовательно, если S содержит пустые предложения, формула (2) является ложью, а это показывает, что B выводится из группы предикатов A1, … , An, то есть из .

4.2.3.1 Метод резолюций для логики высказываний

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

Предположим, что в множестве предложений есть дополнительные литералы (которые отличаются только символами отрицания L и ) вида:

Исключим из этих двух предложений дополнительные литералы и представим оставшуюся часть в дизъюнктивной форме (такое представление называется резольвентой):

После проведения этой операции легко видеть, что C является логическим заключением C_i и C_j. Следовательно, добавление C к множеству S не влияет на вывод об истинности или ложности S. Если выполняется C_i = L, то C пусто. То что C является логическим заключением из S и C пусто, указывает на ложность исходной логической формулы.

Приведем простой пример такого доказательства:

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

- пустое предложение.

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

Такая структура называется дедуктивным деревом или деревом вывода.

4.2.3.2 Принцип резолюции для логики предикатов

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

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

Целью унификации является обеспечение возможности применения алгоритма доказательства для предикатов. Например, предположим имеем:

В данном случае 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)).

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

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

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

3. Первые несовпадающие элементы {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 - принцесса.

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

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

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

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

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

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

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

Удалим квантор существования из предложений 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 - упорядочивания.