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

Метод резолюции в ЛВ.

Читайте также:
  1. Battement tendu. Методика преподавания, виды.
  2. I. Задачи и методы психологии народов.
  3. II. Метод они должны иметь поистине универсальный, где нужно соблюдать следующее.
  4. III. Методы строительства
  5. IV. Изучите методику объективного обследования.
  6. IV. Методические указания студентам по подготовке к занятию
  7. PEST-аналіз як ефективний метод дослідження макросередовища діяльності підприємства.

Пусть C1 и C2 – клозы. Клоз C1ÚC2 называется бинарной резольвентой (или просто резольвентой)клозов C1Ú p, C1Úùp.

Например, pÚqÚùl pÚùlÚf

ùqÚf

Литеры p, ùp при этом называются контрарными.

Доказано, что резольвента является логическим следствием.

Замечание.Клоз можно рассматривать как множество литер. Так клоз pÚùlÚf фактически есть множество литер {p,ùl, f}. Таким образом, мы приходим к понятию пустого клоза ().

Метод резолюции сводится к последовательному получению резольвент, каждая из которых является логическим следствием. Из данного множества клозов (так называемого входного множества) пытаются вывести пустой клоз. Этот процесс называется резолютивным выводом пустого клоза или опровержением множества клозов.

Например:

Дано: p®q

q®f

Доказать: p®f

Доказательство: 1) Приводим все формулы к КНФ: ùpÚq, ùqÚf

ù(p®f)= ù(ùpÚf)=pÙùf

2) Производим резолюцию:

  ùpÚq ùpÚf f
 
 

 

 
  ùqÚf p ùf
  p ùf  
  ùf    

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

Читайте в этой же книге: Введение | Точка зрения Петрунина. | Данные и знания. Основные модели представления знаний | Метод резолюции в ЛППП. | Стратегии проведения резолюции. | Упорядоченный линейный вывод в ЛППП. | Применение поиска в пространстве состояний при реализации автоматизированного логического вывода. | Логический вывод на хорновских дизъюнктах. | Понятие экспертной системы и применение логического вывода при построении экспертных систем. | Запросы класса C. |
<== предыдущая страница | следующая страница ==>
Булева алгебра.| Основные определения.
mybiblioteka.su - 2015-2024 год. (0.005 сек.)