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

Резольвенция и факторизация



Читайте также:
  1. И экеппораторная факторизация 1 страница
  2. И экеппораторная факторизация 2 страница
  3. И экеппораторная факторизация 3 страница
  4. И экеппораторная факторизация 4 страница

При доказательстве теорем в математической логике используются представления суждений в виде дизъюнкции литералов (в виде предложений, в клаузальной форме). Литерал L1 называется дополнительным литералу L2, если L1 является отрицанием L2.

Резольвента двух предложений получается следующим образом [29]:

1) переменные одного предложения переименовываются таким образом, чтобы они отличались от переменных другого предложения;

2) находится подстановка, при которой какой-либо литерал одного предложения становится дополнительным к какому-либо литералу другого предложения и эта подстановка производится в оба предложения;

3) литералы, дополнительные друг к другу, вычёркиваются;

4) если имеются одинаковые литералы, то все они, кроме одного в каком-либо предложении вычёркиваются;

5) дизъюнкция литералов, оставшихся в обоих предложениях, и есть резольвента.

Используется также факторизация. Фактором какого-либо предложения называется следствие этого предложения [29]:

1) находится подстановка при которой какие-либо литералы одинаковы;

2) после выполнения этой подстановки все одинаковые литералы, кроме одного, вычёркиваются;

3) дизъюнкция оставшихся литералов и есть фактор.

Процесс нахождения фактора называется факторизацией.

Пример [29].

Резольвента при подстановке {(g(x),x}, то есть g(x) заменяет x.

.

Здесь резольвенты нет. Переменные: x, y – термы: g(x), f(x).

Вместо переменной можно подставить терм, но вместо функции или константы терм подставить нельзя!

Пример [26].

{P(x,a,f(g(a))),P(z,y,f(u))}.

В этом случае наименьший общий унификатор: {(z,x),(a,y),(g(a),u)}.

Просто унификатор: {(b,x),(a,y),(b,z),(g(a),u)}.

 


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






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