Лекции по дискретной математике. Математическая логика. Зарипова Э.Р - 55 стр.

UptoLike

ВУЗ: 

РУДН | Москва

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

Рубрика: 

55
необходимо.
Шаг 4
. Используем эквивалентности (12.1)-(12.6), (12.11),
(12.12).
Пример 12.1.
Привести к предваренной нормальной форме
формулу (
∀x)P(x)
→
(∃x)Q(x).
))()()(()()()()(
)()()()()()()()(
xQxPxxQxxPx
xQxxPxxQxxPx
∨∃=∃∨∃=
=∃∨∀=∃→∀
Пример 12.2.
Привести к предваренной нормальной форме
формулу
(
∀x) (∀y)(((∃z)P(x,z)
∧
P(y,z))
→
(∃u)Q(x,y,u)).
( )( )((( ) ( , ) ( , )) ( ) ( , , ))
()()((()(,) (,))()(,,))
( )( )((( )( ( , ) ( , )) ( ) ( , , ))
()()()()((,) (,) (,,)).
xy zPxzPyz uQxyu
xy zPxzPyz uQxyu
xy zPxzPyz uQxyu
xyzuPxzPyzQxyu
∀∀ ∃ ∧ →∃ =
∀∀ ∃ ∧ ∨∃ =
∀∀ ∀ ∨ ∨∃ =
∀∀∀∃ ∨ ∨
13. Скулемовская стандартная форма. Подстановка и
унификация. Алгоритм унификации.
Скулемовская стандартная форма.
Пусть формула F находится в предваренной нормальной форме
(Q
1
x
1
)…(Q
n
x
n
)M. Пусть Q
r
есть квантор существования в префиксе
(Q
1
x
1
)…(Q
n
x
n
),1
≤
r
≤
n. Если никакой квантор всеобщности не
стоит в префиксе левее Q
r
, выбираем константу C, отличную от
других констант, входящих в M, заменяем все x
r
, встречающиеся в
M, на C и вычеркиваем (Q
r
x
r
) из префикса. Если
m1
ss
QQ ,..., -
список всех кванторов всеобщности, встречающихся левее
,..., rsss1Q
m21r
<<
<
≤
выбираем новый m- местный
функциональный символ f, отличный от других функциональных
символов из M, заменяем все x
r
из M на ),...,,(
m21
sss
xxxf и
вычеркиваем (Q
r
x
r
) из префикса. Применяем эту процедуру для
всех кванторов существования, имеющихся в префиксе формулы
F. Последняя из полученных формул есть скулемовская

Страницы