Аналитико-табличный метод в логике предикатов.




Используется для решения задач, не решаемых методом перебора моделей. По сути - стандартизация рассуждения от противного, оформленная в виде таблицы.

Метод от противного – допускаем, что тезис не верен, сводим рассуждение к противоречию и получаем, тезис верен.

Используется для обоснования тезисов об

- общезначимости А (антитезис А)

- невыполнимости А (антитезис - сама А)

- отношении логического следования Г ╞ B (антитезис - Г, B)

- несовместимости по истинности А12,…,Аn (антитезис - А12,…,Аn)

- несовместимость по ложности А12,…,Аn (антитезис - А1, А2,…, Аn)

 

Правила редукции:

[&] Г, А&В, ∆ [ &] Г, (А&В), ∆.

Г, А, В, ∆ Г, А, ∆ | Г, B, ∆

 

[ ] Г, А В, ∆ [ ] Г, В), ∆

Г, А, ∆ | Г, А, ∆ Г, А, В, ∆

 

[ ] Г, А В, ∆ [ ] Г, В), ∆

Г, A, ∆ | Г, В, ∆ Г, А, В, ∆

 

[ ] Г, А, ∆

Г, А, ∆

 

[ ] Г, αA, ∆ [ ] Г, αA, ∆

Г, αA, А(t), ∆ Г, А(k), ∆

 

[ ] Г, α А,∆ [ ] Г, α А, ∆.

Г, А(k), ∆ Г, α А, А(t), ∆

Определения:

Стока аналитической таблицы (конфигурация) – непустое множество непустых формульных списков

Аналитическая таблица – последовательность конфигураций, такая, ято каждая следующая конфигурация получается из предыдущей заменой формул по правилам редукции

Замкнутый формульный список - содержащий А и А

Замкнутая конфигурация – состоящая из замкнутых списков

Замкнутая таблица – содержащая конечное число конфигураций, последняя из

которых замкнута

Цель построения таблицы – получить замкнутую конфигурацию

 

Критерии:

Общезначимости

Формула А общезначима, если, и только если существует замкнутая аналитическая таблица, первая конфигурация которой содержит единственный формульный список - А.

Невыполнимости

Формула А невыполнима, если, и только если существует замкнутая аналитическая таблица, первая конфигурация которой содержит единственный формульный список - А

Отношения логического следования

Из формул А12,…,АnВ если, и только если существует замкнутая аналитическая таблица, первая конфигурация которой содержит единственный формульный список - А12,…,Аn В

Несовместимости по истинности

Формулы А12,…,Аn совместимы по истинности если, и только если существует замкнутая аналитическая таблица, первая конфигурация которой содержит единственный формульный список - Фрейд, Юнг, Выготский, Леонтьев,

Несовместимости по ложности

Формулы А12,…,Аn совместимы по ложности если, и только если существует замкнутая аналитическая таблица, первая конфигурация которой содержит единственный формульный список А1, А2,…, Аn

 

 

6. Аксиоматическое исчисление предикатов: схемы аксиом и правила вывода, понятия доказательства, вывода и теоремы.
Определение исчисления – см. выше

Дедуктивные постулаты:

- аксиомы (формулы языка, которые постулируются в качестве законов)

- правила вывода.

Все постулаты исчисления высказываний сохраняются, но добавляются еще новые аксиомы и правила.

Два способа построения –

1. с конечным числом аксиом и правилами подстановки

2. с бесконечным числом аксиом и их схемами

Использующийся язык – язык логики предикатов, но квантор только один -

Квантор существования может быть введен по определению: αA ≡Df α A

 

Схемы аксиом (A1 – A12)

1. А (B A) – схема консеквента

2. (A (B C)) ((A B) (A C)) - схема самодистрибутивности

3. A (B (A&B)) - схема введения &

4. (A&B) A - 1-ая схема исключения &

5. (A&B) B - 2-ая схема исключения &

6. A (A B) - 1-ая схема введения

7. B (A B) - 2-ая схема введения

8. (A B) ( A B) – схема исключения

9. (A B) ((A B) A) - схема введения

10. A A - схема исключения

11. αA A(t) - схема исключения

12. α (A B) (A αB) - схема пронсения через

Правила вывода:

R1 A B, A - modus ponnens

B

R2 A -правило генерализации

αA

Особенности:

1. Если R2 применять к закону, то в результате получается закон. Если оно применяется не к закону, то на него накладываются ограничения.

2. Формулы вывода зависят от допущений.

3. Каждое допущение зависит от самого себя.

4. Аксиомы не зависят от допущений.

Доказательство – непустая конечная последовательность формул, такая что каждая формула этой последовательности есть или аксиома, или ф-ла полученная по правилу mp, или полученная по правилу генерализации.

Доказательство формулы А – доказательство, последней формулой которого является А.

Теорема (закон) – формула, для которой существует доказательство.

Вывод из Г – непустая конечная последовательность формул С12,…,Сn, такая, что каждая С iесть либо допущение из Г, либо аксиома, либо формула полученная в результате применения R1, либо формула полученная в результате применения R2

Ограничение: формула VαA может быть получена из А (по R2), зависящей от множества допущений в том случае, когда α не содержится свободно ни в одной формуле из , ни в одном допущении из ∆.

Отношение выводимости Г├B. Формула В выводима из множества допущений Г если и только если существует вывод из множества допущений Г, последней формулой которого является В.

 




Поделиться:




Поиск по сайту

©2015-2024 poisk-ru.ru
Все права принадлежать их авторам. Данный сайт не претендует на авторства, а предоставляет бесплатное использование.
Дата создания страницы: 2016-04-26 Нарушение авторских прав и Нарушение персональных данных


Поиск по сайту: