Математическое введение в декларативное программирование. Зюзысов В.М. - 37 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

мулу A
3
, которая
не содержит кванторов и формулы A
2
и A
3
одновременно выполнимы
или невыполнимы.
4. Приведение к конъюнктивной нормальной форме. Выполняем логически эквивалент-
ные преобразования вида: X∨(Y&Z) = (X∨Y)&(X∨Z); После четвертого этапа получаем
формулу A
4
, которая находится в конъюнктивной нормальной форме.
5. Элиминация конъюнкции. Преобразование: X&Y → X, Y. После пятого этапа формула
распадается на множество дизъюнктов.
Теорема 10. Если Γ − множество дизъюнктов, полученных из формулы A, то A яв-
ляется противоречием тогда и только тогда, когда множество Γ невыполнимо.
(Множество формул Γ невыполнимо − это означает, что множество Γ не имеет модели, то
есть не существует интерпретации, в которой бы все формулы Γ имели бы значение И.)
Доказательство. Формулы A и A
4
одновременно выполнимы или невыполнимы в
любой интерпретации. Формула A
4
является противоречием тогда и только тогда, когда
Γ не имеет модели.
6.6 Правило резолюции для исчисления высказываний
Пусть C
1
и C
2
− два дизъюнкта в исчислении высказываний, и пусть C
1
= P∨A, а C
2
= ¬P∨B, где P − пропозициональная переменная, а A, B − любые дизъюнкты (в частности,
может быть, пустые или состоящие только из одного литерала). Правило вывода
R
BA
CC
∨
21
,
называется правилом резолюции. Дизъюнкты C
1
и C
2
называются резольвируемыми (или
родительскими), дизъюнкт A∨B − резольвентой, а формулы P и ¬P − контрарными лите-
ралами.
Правило резолюции − это очень мощное правило вывода. Многие правила вывода
являются частными случаями правила резолюции:
ponensModus
B
BAA
⊃
,
R
B
BAA ∨¬,
остьТранзитивн
CA
CBBA
⊃
⊃⊃
,
R
CA
CBBA
∨¬
∨¬∨¬ ,
Доказательство следующей теоремы тривиально.
Теорема 11. Резольвента является логическим следствием резольвируемых дизъ-
юнктов.
6.7 Унификация
Пусть имеются две элементарные формулы A и B языка первого порядка. Эти фор-
мулы могут содержать индивидные (предметные) переменные. В некоторых случаях воз-
можна такая подстановка термов вместо переменных в этих формулах, что формулы A и B
(вообще говоря, различные) становятся тождественными. Такая подстановка называется
унификатором. Например, формулы F(x, p(x,y)) и F(t(z,c),u) можно унифицировать: для
этого достаточно переменную x заменить на t(z,c), а вместо переменной u подставить терм
p(t(z,c),y); в результате унификации получаем формулу F(t(z,c), p(t(z,c),y)).
В общем случае под подстановкой мы понимаем множество θ = {t
1
/X
1
, ..., t
n
/X
n
},
где все X
i
(i=1,..., n) – различные переменные, а t
i
– термы, отличные от всех X. Результат
применения подстановки θ к элементарной формуле E (т. е. результат одновременной за-
мены всех переменных X
1
, ..., X
n
на термы t
1
, ..., t
n
соответственно) обозначается Eθ. Ком-
позиция θλ подстановок θ и λ определяется естественным образом и удовлетворяет усло-
вию (Eθ)λ = E(θλ) для любой формулы E.
37

Страницы