Конспект установочных лекций по комплексному курсу Информатика, Теория информации



         

Логическое программирование - часть 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), однако обратное, вообще говоря, неверно.

Унификация

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

Унификация является операцией на множестве термов. Результатом унификации является подстановка, которая для каждого терма заданного множества в качестве результата выдает один и тот же терм. Такая подстановка называется унификатором. Но, не для каждого множества существует такого рода унификатор - в этом случае множество называется не унифицируемым.




Содержание  Назад  Вперед