Главная страница | Контакты | Случайная страница Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

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

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

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

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

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

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

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

- несовместимости по истинности А₁,А₂,…,А_n (антитезис - А₁,А₂,…,А_n)

- несовместимость по ложности А₁,А₂,…,А_n (антитезис - А₁, А₂,…, А_n)

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

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

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

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

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

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

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

[ ] Г, А, ∆

Г, А, ∆

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

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

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

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

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

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

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