Математическая логика и теория алгоритмов. Анкудинов Г.И - 45 стр.

UptoLike

ВУЗ: 

СЗТУ | Санкт-Петербург

Составители: 

Рубрика: 

Клаузы Хорна и метод резолюций
Клаузой Хорна называется частный случай клаузы
B
,...,B
m
←A ,...,A , получающийся при m=1:
n
B
1 1
B
,...,A
B ← A
.
n1
Метод резолюций основан на использовании правил резолюции.
Правило резолюции – это правило вывода, которое позволяет из двух
предложений
B
,...,B
m
← A ,...,AB
1
B
1 i
,...,A и
n
,...,B'
B'
1 j
,...,B'
r
← A' ,...,A'
k
,
1
для которых существует так называемая согласующая подстановка σ
такая, что A
i
σ=B'
j
σ, вывести третье
σ,..., B
m
σ, B' σ,..., B' σ, B' σ,..., B'
B
B
1
B
1 j-1 j+1 r
σ ←
σ,..., A σ, A σ,..., A σ, A' σ,..., A'
A
1 j-1 j+1 n k
σ.
1
Понятие согласующей подстановки σ определяется как
множество пар {(x
,t )}, означающих, что переменная x всюду в A
q q q i
и
B'
заменяется термом t так, что A
j q i
σ=B'
j
σ, причем любая другая
унифицирующая подстановка θ носит менее общий характер.
Для клауз Хорна правило резолюции можно записать в общем
виде
,A ,...,A | B' ← A' ,...,A'
B ← A
n k1 2 1
A σ=B' σ,
1 1
σ,...,A'
Bσ ← A'
1 k
σ, A σ,...,A σ
n2
где σ - согласующая подстановка, | - разделитель клауз.
Сущность метода резолюций – это процедурная интерпретация
клауз Хорна, которая заключается в следующем. Множество клауз
Хорна S, описывающих постановку задачи, дополняется отрицанием
C← целевого утверждения C, содержащего в общем случае
некоторые предметные переменные, значения которых необходимо
определить. С помощью правил резолюции находим решение задачи,
а именно значения предметных переменных, для которых
множество S ∪ {C←} невыполнимо. Это значения предметных
129

Страницы