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

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 29 из 64
© 2003 Галуев Геннадий Анатольевич
Рассмотрим, что это за форма.
Пусть формула
A
находится в предваренной нормальной форме MxQQxQx
nn
...
21
,
где формула
M
без кванторов в конъюнктивной нормальной форме (конъюнкция
дизъюнкций (
)...)(&)(
2121
XVXVXX ⎤ .
Пусть
r
Q - квантор существования )(
∃
в префиксе
nn
XQXQ ...
1¬
)1( nr ≤≤ . Если ни-
какой квантор всеобщности
)(∀ не стоит в префиксе левее
r
Q , выберем новую кон-
станту
c , отличную от других констант, входящих в
M
; заменим все
r
x , входящие в
M
на c и вычеркнем
rr
xQ из префикса.
Если
sms
QQ
...,,1
- список всех кванторов всеобщности )(
∀
, встречающихся левее
r
Q )1(
...,,1
rSS
m
≤〈≤ , выберем новый
m
местный функциональный символ
m
f , отлич-
ный от других функциональных букв, заменим все
r
X в
M
на )(
...,1 sms
xxf и вычеркнем
rr
XQ из префикса. Затем весь этот процесс применим для
оставшихся кванторов существования в префиксе
nn
XQXQ ...,,
11
. Тогда последняя по-
лученная в результате этой процедуры формула есть скулемовская стандартная фор-
ма формулы A . Константы C и функции
m
f , используемые для замены переменных
кванторов существования, называются скулемовскими
.
Таким образом, в префиксе стандартной (скулемовской) формы кванторы суще-
ствования отсутствуют.
Например: Приведем формулу вида
),(),( ZXQYPXzyx →∃∃∀
к скулемовской стандартной форме. Приведем матрицу
M
к конъюнктивной нор-
мальной форме
)),(),(( zxQyxPzyx ∨⎤∃∃∀
Затем, так как перед кванторами
y
∃
и z
∃
есть один квантор
x∀
, то переменные
y и
z
заменяются соответственно одноместными функциями
)
xf и )(xg
)).(,())(,((( xgxQxfxPx ∨⎤∀
Отметим, что вид функций
f и
g
, использованных в этом примере, явно не оп-
ределяется, что приводит к неединственности стандартных форм (скулемовских) при
выборе того или иного вида скулемовских функций.
Введем следующие определения.
• Литера есть элементарная формула или ее отрицание.
• Дизъюнкт есть дизъюнкция литер. Дизъюнкт, содержащий
r
литер, назы-
вается
r
- литерным дизъюнктом. Однолитерный дизъюнкт называется еди-
ничным дизъюнктом.
Если дизъюнкт не содержит литер он называется пустым дизъюнктом
. Так как
пустой дизъюнкт не содержит литер, которые могли бы быть истинными, то пустой
дизъюнкт всегда ложен
и обозначается как O .
Множество дизъюнктов из
S есть конъюнкция всех дизъюнктов из S , где каждая
переменная из
S считается управляемой квантором всеобщности )(∀ . Благодаря это-
му соглашению стандартная форма (скулемовские) может быть представлена множе-
ством дизъюнкторов.
Например: стандартная форма
))())(,((&))())(,(( xRxgxQxRxfxPx ∨∨⎤∀
может быть представлена множеством
}
{
)()(,(),())(,( xRxgxQxRxfxP ∨∨⎤ .

Страницы