Сводка определений и основных фактов (1157988), страница 3
Текст из файла (страница 3)
. При этом
называется сколемовской функцией.
Определение. Система дизъюнктов S называется невыполнимой, если не существует такой интерпретации, в которой будут выполнимы одновременно все дизъюнкты, входящие в S.
Теорема. Формула ϕ общезначима тогда и только тогда, когда невыполнима система дизъюнктов
.
О
п
р
е
д
е
л
е
н
и
е
.
О
с
н
о
в
н
ы
м
т
е
р
м
о
м
н
а
з
ы
в
а
е
т
с
я
л
ю
б
о
й
т
е
р
м
,
н
е
и
м
е
ю
щ
и
й
с
в
о
б
о
д
н
ы
х
п
е
р
е
м
е
н
н
ы
х
.
Определение. Эрбрановским универсумом (Н) называется множество основных термов, которое строится следующим образом:
1.
2.
для всех 
и
3.
Определение. Эрбрановской интерпретацией для системы дизъюнктов Sϕ называется интерпретация
, где H – эрбрановский универсум, а остальные множества определяются следующим образом: 
Теорема (об эрбрановских интерпретациях): Система дизъюнктов невыполнима тогда и только тогда, когда она невыполнима на эрбрановских интерпретациях.
Существует несколько способов представления эрбрановских интерпретаций:
1. Теоретико-множественный.
Назовем основным атомом атомарную формулу (без свободных переменных), полученную в результате подстановки в некоторый предикат Р основных термов:
Тогда I будет являться эрбрановской интерпретацией для множества основных атомов, если на ней будет выполним любой основной атом из этого множества.
2. Последовательный
Основной литерой называется либо основной атом, или его отрицание. Упорядоченное множество всех основных атомов будет называться эрбрановским базисом В. Тогда с эрбрановской интерпретацией можно связать последовательность литер , причем
будет равно , если выполнима в I, и
в противном случае.
Определение. Пусть - эрбрановский базис. Семантическим деревом называется бинарное корневое дерево следующего вида (см. рисунок слева).
В таком дереве каждая ветвь соответствует какой-нибудь эрбрановской интерпретации.
С помощью семантического дерева можно легко сформулировать критерии выполнимости системы дизъюнктов.
Определение. Основным примером дизъюнкта
будет называться подстановка 
, где
.
У
т
в
е
р
ж
д
е
н
и
е
.
С
и
с
т
е
м
а
д
и
з
ъ
ю
н
к
т
о
в
н
е
в
ы
п
о
л
н
и
м
а
т
о
г
д
а
и
т
о
л
ь
к
о
т
о
г
д
а
,
к
о
г
д
а
д
л
я
л
ю
б
о
й
э
р
б
р
а
н
о
в
с
к
о
й
и
н
т
е
р
п
р
е
т
а
ц
и
и
,
к
о
т
о
р
а
я
з
а
д
а
н
а
в
в
и
д
е
п
о
с
л
е
д
о
в
а
т
е
л
ь
н
о
с
т
и
л
и
т
е
р
,
с
у
щ
е
с
т
в
у
е
т
т
а
к
о
й
о
с
н
о
в
н
о
й
п
р
и
м
е
р
D'
д
и
з
ъ
ю
н
к
т
а
D
и
з
э
т
о
й
с
и
с
т
е
м
ы
,
ч
т
о
,
ч
т
о
д
л
я
н
е
к
о
т
о
р
ы
х
е
г
о
к
о
м
п
о
н
е
н
т
б
у
д
е
т
в
ы
п
о
л
н
я
т
ь
с
я
р
а
в
е
н
с
т
в
о
, т.е. всегда будет находиться ложный основной пример.
Определение. Пусть v – вершина семантического дерева, в котором из корня ведет путь, помеченный литерами . Пусть также дизъюнкт D принадлежит системе S
ϕ . Говорят, что дизъюнкт D опровергается в вершине v, если существует такой основной пример D', состоящий из литер , причем любая литера ' из D будет равна . 
Определение. Вершина v называется опровергающим узлом для системы дизъюнктов Sϕ , если
1) в вершине v опровергается какой-нибудь дизъюнкт D из Sϕ ;
2) никакая другая вершина, лежащая выше на пути из корня к v не опровергает ни одного дизъюнкта.
Лемма (о семантическом дереве): Система дизъюнктов невыполнима тогда и только тогда, когда в ее семантическом дереве каждая ветвь содержит опровергающий узел, и число таких узлов конечно.
Лемма (Кенига): Если есть бесконечное семантическое дерево, и из каждой его вершины выходит конечное число дуг, то это дерево содержит бесконечную ветвь.
Теорема (Эрбрана; об основных примерах): Система дизъюнктов S невыполнима (противоречива) тогда и только тогда, когда существует конечное множество S' основных примеров дизъюнктов из S, такое, что S' – тоже противоречивое множество.
Теорема Эрбрана сводит проблему выполнимости системы дизъюнктов к исследованию истинности булевых формул.
Алгоритм Девиса-Паттена проверки противоречивости системы дизъюнктов.
1. Строим семантическое дерево
2. Порождаем основные примеры дизъюнктов из системы.
После этого проверяется опровержимость основных примеров в вершине семантического дерева. Алгоритм завершается успешно, если построенная система опровергающих узлов пересекает все дерево.
Определение. Композицией конечных подстановок
и 
называется такая конечная постановка
, что для любой переменной x
. Композиция подстановок обозначается как
.
Определение. Подстановка
называется унификатором для логических выражений , если 
.
Определение. Подстановка
называется наиболее общим унификатором (НОУ) для логических выражений , если 
1)
- унификатор для ; 
2)
д
л
я
л
ю
б
о
й
п
о
д
с
т
а
н
о
в
к
и
, которая тоже унифицирует найдется такая подстановка
, что
(т.е.
является частным случаем
).
Определение. Наиболее общим унификатором для системы уравнений вида для атомарных формул и
называется такая подстановка
, что:
1) выполняется система равенств
;
2) любая другая подстановка, для которой эта система также выполняется, является частным случаем
.
Утверждение.
- НОУ для формул 
и
тогда и только тогда, когда
является НОУ для системы уравнений для этих формул.
Лемма (о связке): Пусть x – переменная, а t – терм, причем х не является свободной переменной для t. Тогда если конечная подстановка
является унификатором x и t (т.е. 
), то
.
Следствие. Подстановка
из условия леммы является НОУ для x и t.
Теорема (о приведенной системе уравнений): Если
- приведенная система уравнений, причем ни один x не является свободной переменной для любого t из системы, то НОУ такой системы 
Алгоритм унификации Мортелло-Мортанари
Дана система термальных уравнений
. Алгоритм решает ее методом подстановки.
До тех пор, пока возможно, выполнить следующие действия:
Выбрать произвольное уравнение и применить к нему одно из 6 правил:
1) если уравнение имеет вид
, то оно преобразовывается в k уравнений ; 
2) если уравнение имеет вид
, причем 
, то алгоритм останавливается с ошибкой;
3) если уравнение имеет вид , где c и k – константы, или x=x, где х – переменная, то такое уравнение надо удалить;
4)
е
с
л
и
у
р
а
в
н
е
н
и
е
и
м
е
е
т
в
и
д
,
г
д
е
y
–
п
е
р
е
м
е
н
н
а
я
,
а
t
–
т
е
р
м
,
т
о
э
т
о
у
р
а
в
н
е
н
и
е
з
а
м
е
н
я
е
т
с
я
н
а
;
5) если уравнение имеет вид
, причем y не является свободной переменной для si, но встречается в каких-нибудь уравнениях 
, то в них надо произвести замену
.
6) если уравнение имеет
, и при этом y является свободной переменной для si, то алгоритм останавливается с ошибкой.
Теорема: Алгоритм унификации завершается и работает корректно, т.е.:
1. для любой системы уравнений l алгоритм останавливается после применения к этой системе;
2. если эта система унифицируема, то алгоритм выдает приведенную систему l’, такую, что ее НОУ совпадает с НОУ исходной системы;
3. если эта система не унифицируема, то алгоритм останавливается с ошибкой.
Определение. Правило резолюции для двух дизъюнктов
и и их НОУ 
- это вывод их резольвенты – дизъюнкта вида
.
Определение. Правило склеивания для дизъюнкта
и НОУ 
для L и L' – это вывод склейки D по паре L и L' – дизъюнкта вида
.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
