Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Логическое программирование - часть 2
Пусть задано правило
С <= B1 Ù ... Ù Bk, (R)
являющееся частью логической программы. Пусть надо доказать (или опровергнуть) условие
fake <= S1Ù ... Ù
Sn. (G)
Правило (R) применимо к условию (G), если существует подстановка с
C[t1/X1, ..., tm/Хm] = Sj[t1/X1, ..., tm/Хm].
Другими словами, общая справедливость (G) опровержима (ведет к противоречию), если условие
~ ~ ~ ~ ~ ~
false <= S1Ù ... Ù Sj-1ÙB1Ù…ÙBkÙSj+1Ù… ÙSn (G )
опровержимо с
~
Si = Si[t1/X1, ..., tm/Хm],
~
Bi=Bi[t1/X1, ...tm/Xm].
Эту редукцию подцели к модифицированной редукции с помощью применения правила назовем резолюцией.
~
Если (G ) опровержимо, то опровержимо также и (G), однако обратное, вообще говоря, неверно.
Унификация
При выполнении логических программ путем применения правил преобразования типичными являются операции над термами. Примером этому служит вопрос о применимости некоторого правила. На этот вопрос можно ответить с помощью методики унификации.
Унификация является операцией на множестве термов. Результатом унификации является подстановка, которая для каждого терма заданного множества в качестве результата выдает один и тот же терм. Такая подстановка называется унификатором. Но, не для каждого множества существует такого рода унификатор - в этом случае множество называется не унифицируемым.
