<<
>>

4.3.Правило резолюции для исчисления высказываний

Пусть С1 и С2 – предложения в исчислении высказываний.

Пусть , , где Р – пропозициональная переменная, - любые предложения.

Правило вывода называется правилом резолюции, где

С1, С2 - родительские предложения,

- резольвента,

- контрарные литералы.

Правило резолюции очень мощное правило вывода и многие ранее рассмотренные правила являются частным случаем правила резолюции.

Примеры.

1. Правило вывода modus ponens:

2. Правило транзитивности

Унификация

Если в формулу А вместо переменных подставить формулы , то получится формула В, которая является частным случаем формулы А.

.

Набор подстановок называется унификатором.

Таким образом, унификация состоит в том, что мы пытаемся сделать одинаковыми различные предикаты.

<< | >>
Источник: Викентьева О. Л.. Математическая логика и теория алгоритмов. Конспект лекций для студентов специальностей АСУ, ЭВТ, КЗИ. Пермь, 2007г.. 2007

Еще по теме 4.3.Правило резолюции для исчисления высказываний:

  1. Список сокращений
  2. ПРОБЛЕМА АВТОРСТВА И ПРАВИЛЬНОСТИ ТЕКСТА ЛИТЕРАТУРНОГО ПРОИЗВЕДЕНИЯ
  3. «Разум и верное исчисление»: представления П.И. Шувалова о собственной деятельности
  4. § 2. Мошенничество
  5. 4.2. ЧАСТНЫЕ ИСКУССТВА РЕЧИ. ДИПЛОМАТИКА, ПИСЬМОВНИКИ, ПРАВИЛА ДЛЯ СОСТАВЛЕНИЯ СОЧИНЕНИЙ (ПОЭТИКА И РИТОРИКА)
  6. 4.3.Правило резолюции для исчисления высказываний
  7. 4.4. Правило резолюции для исчисления предикатов
  8. ДОКАЗАТЕЛЬСТВО ТЕОРЕМ НА ОСНОВЕ ПРИНЦИПА РЕЗОЛЮЦИИ