X  y, (X → y)  u, z → (y → w)  (w → X) → (z  X).

Приведем ее в соответствующую конъюнктивно-дизъюнктивную нормальную форму:

X  y, X y  u,zy w  w X;z; X.

Далее разобьем первый дизъюнкт, в результате получим две производные клаузы: 1. X, X Y  U,ZY W  W X;Z; X , 2. Y,X Y  U,ZY W  W X;Z; X .

Клауза (1) отбрасывается, так как она удовлетворяет клаузе Вонга. Разбивая дизъюнкт клаузы (2), получаем еще три клаузы:  2.1. Y, X,ZY W  W X;Z; X, 2.2. Y, Y,ZY W  W X;Z; X, 2.3. Y, U,ZY W  W X;Z; X.

Клаузы (2.1) и (2.2) сводятся к одной клаузе —  2.1. Y, ZY W  W X;Z; X.

Разобьем ее:  2.1.1. Y, Z W X;Z; X, 2.1.2. Y,Y W X;Z; X, 2.1.3. Y, W  W X;Z; X.

Первые две клаузы удовлетворяют клаузе Вонга. У клаузы (2.1.3) нужно разбивать конъюнкт: 2.1.3.1. Y, W  W; Z; X, 2.1.3.2. Y, W X;Z; X.

Теперь обе клаузы имеют вид клаузы Вонга.

Но у нас осталась еще ветвь (2.3). Она отличается от рассмотренной ветви (2.1) наичием непарного терма U, который, однако, не может повлиять на конечный результат, т.е. разбиение клаузы (2.3) практически полностью совпадает с разбиением клаузы (2.1). Следовательно, исходная клауза была записана верно.

24. Исчисление высказываний. Перенос высказываний через знак выводимости

знак выводимости

Теорема дедукции

Пусть А и В – формулы исчисления высказываний. Тогда если АВ, то АВ

или

Пусть А и В – формулы исчисления высказываний, Г – множество формул исчисления высказываний, тогда если Г,А В, то Г АВ

Например,

АВ,ВС,АС применим теорему дедукции

АВ,ВСАС применим теорему дедукции АВ(ВС)(АС) применим теорему дедукции

(АВ)(ВС)(АС)