Основные равносильности для предикатов.
Для нас имеют смысл и значение только интерпретированные предикаты. То есть предикаты, которым
поставлены в соответствия некоторые отношения (одномерным предикатам – свойства). В результате,
предикаты дают некоторые содержательные высказывания относительно объектов рассматриваемых
областей. Если соответствующее высказывание истинно, то говорят, что оно выполняется в данной
интерпретации.
Предикат называется общезначимым, если он истинен в любой интерпретации.
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 }
Замечание. Другой вариант метаязыка
вместо ::= используется стрелка ® , терминальные символы записываются маленькими (строчными)
буквами, а нетерминальные – большими (прописными) буквами.
Такой вариант мета языка чаще используется в математической литературе. Первый предпочитают
использовать в литературе для программистов. Так что мы будем пользоваться и тем и другим вариантами.