Для нас имеют смысл и значение только интерпретированные предикаты. То есть предикаты, которым
поставлены в соответствия некоторые отношения (одномерным предикатам – свойства). В результате,
предикаты дают некоторые содержательные высказывания относительно объектов рассматриваемых
областей. Если соответствующее высказывание истинно, то говорят, что оно выполняется в данной
интерпретации.
Предикат называется общезначимым, если он истинен в любой интерпретации.
1. "x P(x) º $x P(x) 2.$x P(x) º "x P(x) 3. "x P(x) º $x P(x)
4. $x P(x) º "x P(x) 5. "x P(x) Ú Q) (предикат Q не зависит от x.)
6. "x P(x) & Q º "x (P(x) & Q) 7. $x P(x) Ú Q º $x (P(x) Ú Q)
8. $x P(x) & Q º $x (P(x) & Q) 9. "x Q º Q
10. $x Q º Q 11. "xP(x) & "xR(x) º "x (P(x) & R(x)) 12. $xP(x) Ú $xR(x) º $x (P(x) Ú R(x))
13. "xP(x) Ú "xR(x) ® "x (P(x) Ú R(x)) 14. $x (P(x) & R(x)) ® $xP(x) & $xR(x)
15. "x P(x) º "yP(y) (х, у - из одной предметной области) 16. $x P(x) º $y P(y)
17. "x$y P(x, y) º $x"y P(x, y) 18. "x"y P(x, y) º "x"y P(x, y)
19. $x$y P(x, y) º $x$y P(x, y)
Важное замечание. Рассматриваем только замкнутые предикаты, то естьпредикаты, не содержащие
свободных вхождений переменных.
В общем случае необходимо пройти три этапа:
1. Получить предваренную нормальную форму.
2. Произвести сколемизацию.
3. Получить дизъюнкты.
 | |
 |
Приведение предикатов к НФ. Сколемизация. Дизъюнкты.
Получение дизъюнктов
1.Привести предикат к нормальной форме (ПНФ)
2.Провести сколенизацию
3.Получить дизъюнкт
Vx(ƎyP(x,y v ƎyR(y) -> Q(x) v ƎyF(y))
Vx(⌐ƎyP(x,y) & ⌐ƎyR(y) v Q(x) v ƎyF(y))
Vx(Vy⌐P(x,y) & Vy⌐R(y) v Q(x) v Ǝy F(y)) y замен на z (последние 2 у)
Конфилкт переменных
VxVyƎz(⌐P(x,y) & ⌐R(y) v Q(x) v F(z))
ПНФ – предварительная нормальная форма
Представление предикатов, в которой используется операции дизъюнкт, конъюнкция, отрицание, но
отрицание должно стоять перед элемент. Квант. Все кванторы должны стоять вначале формы
1.Исключить опрации: ипликация, эквивал, и т.д.
2.Перенести отрицание во внутрь формулы
3.Перен. связные переменные и вписать кванторы за скобки
4. Перейти к КНФ (алгебра логики)
Отбрасываем квантор с помощью сколенизации
Пример: (ƎxP(x)vVyQ(y) & (Vx,yR(x,y)vƎyL(y))= (ƎxP(x)vVyQ(y)& (Vz,qR(z,q)vƎdL(d) =
ƎxVyVzVqƎd(P(ac)vq(y) & (R(z,q)vL(fc(y,z,q))
Сколемизация
ƎxP(x) заменить P(ac)
C – индекс константы
VxƎyP(x,y)=P(x,fc(x))
Зависимость функциональная
 | |||
|
8. 
Аксиоматические системы.
Для того чтобы задать аксиоматическую теорию необходимо задать язык, аксиомы и правила вывода
данной теории.
Язык:
а) Символы теории, это
буквы (для определенности, заглавные латинские): A, B, C,..., Z
специальные символы: (,), ®,
б) Последовательности символов образуют выражения.
Например, выражениями будут AB ® (B или другое, более приятное глазу,
(A ® B) ® (B)
Формулами будем называть выражения, задаваемые индуктивно следующим образом:
а) Любая буква (A... Z) есть формула.
б)Если А, В - формулы, то (А), A, A ® B - также формулы.
Аксиомы зададим тремя схемами аксиом:
A ® (A ® B)
(A ® (B ® C)) ® ((A ® B) ® (A ® C))
(A ® B) ® (B ® A)
В схемы аксиом вместо A, B, C могут быть подставлены любые формулы. В результате конкретных
подстановок на основе схем аксиом будут появляться конкретные аксиомы.
Правила вывода: В данной конкретной версии аксиоматической теории используется всего одно (но самое
известное) правило вывода modus ponens
(модус утверждающий) или кратко - mp. Это правило, учитывая особенность его работы, еще называют
правилом отсечения.
A, A ® B ½¾ B
Символ ½¾ читается как "выводимо". То есть в данной теории из формул
A и A ® B выводима формула B или формула B есть теорема данной теории.
Выводом (в данной теории) называется последовательность формул Ф1, Ф2,..., Фn, где каждая следующая
формула является аксиомой, или следует по правилу вывода из предыдущих. Последняя формула вывода
называется теоремой.
Важное замечание. При описании теории, в том числе и ее языка, использовались средства, не
принадлежащие определяемому (целевому) языку: запятые, точки, слова русского языка и т.д.
Совокупность средств, используемых при описании целевого языка, называется метаязыком.
Пример:
Лемма: ½¾ A ® A
Ф1: Возьмем схему аксиом 2 и подставим А = А, С = А, В = А ® А, в результате получим:
(A ® ((A ® A) ® A)) ® ((A ® (A ® A)) ® (A ® A))
Ф2: Из схемы аксиом 1, при А = А, В = А ® А, получим:
(А ® ((А ® А) ® А))
из Ф1,Ф2 по m.p. получаем Ф3: (A ® (A ® A)) ® (A ® A)
Ф4: Из схемы аксиом 1, при А = А, В = А, получим:
(А ® (А ® А))
из Ф3, Ф4 по m.p. получаем Ф5: A ® A
 | |
 |
Формальные грамматики.
Формальная грамматика - это четверка G = <VN,VT, P, S >, в которой
VN - нетерминальный словарь (множество нетерминальных символов);
VT - терминальный словарь (множество терминальных символов);
P - множество грамматических правил;
S Î VN - начальный нетерминальный символ.
Метаязык - язык, с помощью которого описывается язык:
::= - есть по определению;
| - “ исключающее или”;
<... > - внутри – один нетерминальный символ;
[ ] - необязательная часть;
, - запятая – разделитель при перечислении.
Пример: Построим грамматику G1:
<прог>::=<оп> | <оп>; <прог>
<оп>::=<пер>:= <выр>
<пер>::=a | b | c
<выр>::=<пер> | <пер> <зн> <выр>
<зн>::= + | - | * | /
V = VN È VT - обобщенный словарь.
V* - цепочка символов (строка, слово) из обобщенного словаря;
V*N - цепочка символов (строка, слово) из нетерминального словаря;
V*T - цепочка символов (строка, слово) из терминального словаря.
e Î V - пустой символ, входит в обобщенный словарь.
Строка a непосредственно порождает строку b и обозначается: a Þ b,
если a = vxw b = vyw и существует некоторое правило p: x::= y,
где v,w, Î V*, х Î VN, у = V* \ {e}
Строка a порождает строку b и обозначается a Þ* b, когда от строки a можно перейти к строке b с
помощью последовательности непосредственных порождений.
Продолжая пример:
<прог> Þ <оп>; <прог> Þ <оп>; <оп> Þ <пер>:= <выр>; <оп> Þ*
a:= b + c; c:= a + b - c;
Грамматика, использующая процедуры (непосредственного) порождения – порождающая грамматика.
Строка b непосредственно свертывается в строку a и обозначается: a Ü b,
если a = vxw b = vyw и существует некоторое правило p: x::= y,
где v,w, Î V*, х Î VN, у = V* \ {e}
Строка b свертывается в строку a и обозначается a *Ü b, когда от строки b можно перейти к строке a с
помощью последовательности непосредственных свертываний.
Грамматика, использующая процедуры (непосредственного) свертывания –распознающая грамматика.
Строки символов из обобщенного словаря, получающиеся в процессе порождения или свертывания,
называются сентенциальными формами.
Язык L, порождаемый данной грамматикой G - множество нетерминальных цепочек, порождаемых из
начального нетерминального символа. Такие терминальные цепочки называются предложениями
данного языка.
L(G) = { x Î V*N | S Þ* x }
Аналогично можно определить язык L через свертывание.
L(G) = { x Î V*N | S *Ü x }
Замечание. Другой вариант метаязыка
вместо::= используется стрелка ®, терминальные символы записываются маленькими (строчными)
буквами, а нетерминальные – большими (прописными) буквами.
Такой вариант мета языка чаще используется в математической литературе. Первый предпочитают
использовать в литературе для программистов. Так что мы будем пользоваться и тем и другим вариантами.
 | |
 |
