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

Метод резолюций



Читайте также:
  1. I. Внесение сведений в форму ДТС-1 при использовании метода определения таможенной стоимости по цене сделки с ввозимыми товарами
  2. I. Флагелляция как метод БДСМ
  3. II. Внесение сведений в форму ДТС-2 при использовании метода определения таможенной стоимости по цене сделки с идентичными товарами
  4. II. Методика работы со стилями
  5. II. Методы и методики диагностики неосознаваемых побуждений.
  6. II. Организационно-методическое и информационное обеспечение олимпиады
  7. II. Організаційно-методичні вказівки

 

Если имеются два высказывания: которые имеют контрарные или инверсные () литералы, то следствием из этих посылок является (BÚC). Проверим это утверждение:

Такие следствия называются резольвентами (это дизъюнкция членов при контрарных литералах).

Метод основан на получении резольвент. Последовательно получаем резольвенты исходного множества формул, доказательство невыполнимости которого мы ведем, до тех пор, пока не получится Æ (пустое следствие). Здесь доказательство ведется от противного.

Для применения этого метода необходимо использовать КНФ. Например, для modus ponens:

Получили дерево доказательства. Взяты две посылки и отрицание заключения в КНФ. Следствием посылок является резольвента B, а следствием является пустое множество Æ. Это признак невыполнимости исходного множества членов КНФ. А т.к. доказательство проводилось от противного, стало быть, мы и доказали следование B из посылок A®B,A.

 


Дата добавления: 2015-07-11; просмотров: 80 | Нарушение авторских прав






mybiblioteka.su - 2015-2024 год. (0.005 сек.)