Главная страница Случайная страница
Разделы сайта
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Б) присоединиь к ним с помощью импликации дизъюнкцию подформул, для ко- торых имеются их отрицания;
|
|
в)снять отрицания перед кванторами.
6.Снять кванторы и предметные переменные..
7.Полученный результат проверить либо с помощью таблиц истинности, либо посредством сведения результата к КНФ.
Обратимся к примеру. Пусть имеется выражение:
[" x M(x) É Ø P(x)) & $x (S(x) & M(x)] É $x (S(x) & Ø P(x))
Проверим его на общезначимость.
1. [Ø $x (M(x) & P(x)) & $x (S(x) & M(x))] É $x (S(x) & Ø P(x))
(Используя закон 13, в исходной формуле заменили квантор общости на квантор существования, а затем выполнили действия п.2).
2. Ø $x (M(x) & P(x)) & $x (S(x) & M(x)) & Ø $x (S(x) & Ø P(x))
(Заменили консеквент на его отрицание, а импликацию на конъюнкцию).
3. $x (S(x) & M(x)) É [$x (M(x) & P(x)) Ú $x (S(x) & Ø P(x))]
(К формуле без отрицания присоединили с помощью имликации дизъюнкцию формул с отрицанием, но при этом убрали отрицание перед кванторами).
4. (S & M) É [(M & P) Ú (S & Ø P)]
(Убрали кванторы и предметные переменные).
Фактически мы свели исходное выражение к выражению логики высказываний; теперь есть возможность привести его к КНФ.
а) Ø (S & M) Ú [(M & P) Ú (S & Ø P)]
б) Ø S Ú Ø M Ú [(M Ú S) & (M Ú Ø P) & (P Ú S) & (P Ú Ø P)]
в) (Ø S Ú Ø M Ú M Ú S) & (Ø S Ú Ø M Ú M Ú Ø P) &
& (Ø S Ú Ø M Ú P Ú S) & (Ø S Ú Ø M Ú P Ú Ø P).
Все конъюнкты оказались истинными, значит, исходное выражение является общезначимым.
Как уже указывалось, в целом для логики предикатов не существует процедуры разрешения. Но проблема разрешения решена, в частности, для логики одноместных предикатов. Это обстоятельство следует принимать во внимание, обращаясь к рассмотренным процедурам разрешения.
Контрольные вопросы и упражнения.
1. Особенности логики предикатов.
2. Понятие алгебраической системы логики предикатов S4.
3. Структура языка S4.
4. Синтаксис метаязыка S4.
5. Определение терма.
6. Определение формулы.
7. Понятия связанной и свободной переменной.
8. Понятие конгруентной формулы.
9. Структура семантики метаязыка S4.
10. Универсум рассуждения U.
11. Інтерпретационная функция І.
12. Определение интерпретации предметной константы.
13. Определение интерпретации предикаторной константы.
14. Определение интерпртации предметно-функциональной константы.
15. Понятие модели.
16. Процедуры установления значений для формул.
17. Определение условий истинности и ложности элементарных формул.
18. Определение условий истинности и ложности формул, у которых главным знаком
являются пропозициональные связки.
19. Определение условий истинности и ложности формул, у которых главным знаком
является квантор.
20. Типология формул в S4 по их семантическим признакам.
21. Понятие логического закона.
22. Определение необщезначимой формулы.
23. Определение выполнимой формулы.
24. Определение невыпонимой формулы.
25. Логические отношения между формулами в S4.
26. Отношение совместимости по истинности.
27. Отношение совместимости по ложности.
28. Отношение логического следования.
29. Проблема разрешения.
30. Метод аналитических таблиц в логике предикатов.
31. Законы логики предикатов.
32. Процедуры разрешения в логике предикатов.
33. Проверить с помощью аналитических таблиц, являются ли общезначимыми
формулы:
а) $x P(x) É " y P(x);
б) " x (P(x) Ú Q(x)) É (" x P(x) Ú " x Q(x));
в) " x (P(x) Ú Q(a)) É (" x P(x) Ú Q(a));
г) [" x (M(x) É Ø P(x)) & $x (M(x) & (S(x))] É $x (S(x) & Ø P(x))
д) [" x (P(x) É M(x)) & " x (M(x) É (S(x))] É $x (S(x) & P(x)).
34. Применить процедуры разрешения «А» и «В» к формулам:
а) [" x (P(x) É M(x)) & $x (S(x) & Ø M(x))] É $x (S(x) & Ø P(x))
б) [" x (M(x) É Ø P(x)) & " x (M(x) É S(x)] É $x (S(x) & Ø P(x))
в) [$x (P(x) & M(x)) & " x (M(x) É S(x))] É $x (S(x) & P(x))
г) [" x (M(x) É Ø P(x)) & $x (S(x) & M(x))] É $x (S(x) & Ø P(x)).
|
|