Доказательство теоремы методом опровержения

Для доказательства невыполнимости множества предложений пользуются доказательством от противного или опровержением. Доказательство выполнимости множества G®Н, что эквивалентно ùGÚН, это опровержение его невыполнимости, или, что то же самое доказательство невыполнимости ù(ùGÚH), что эквивалентно GÙùH.

Следовательно, на практике пытаются доказать опровержением, что Н является следствием G = G₁Ù...ÙG_n путем до­казательства невыполнимости для G₁,...,G_n и ùН.

Пример 9.6.

Пусть истинны следующие формулы :

программист(Денис)®оптимист(Денис)

программист(Денис)

Требуется доказать, что “Денис” является оптимистом, т.е. истинна формула оптимист(Денис).

Вначале преобразуем эти формулы в предложения:

R₁ : ùпрограммист(Денис)Úоптимист(Денис)

R₂ : программист(Денис)

R₃ : ùоптимист(Денис).

Процедура резолюций состоит в следующем: возьмем R₁ и R₃ и, удалив литерал “оптимист(Денис)” и дополнительный к нему литерал, получим резольвенту “ùпрограммист(Денис)”, ко­торая является дополнительной к предложению R₂, и поэтому в результате удаления последних имеем пустую резольвенту. По­явление последней свидетельствует о том, что исходное множество предложений невыполнимо (противоречиво) и поэтому можно заключить, что наше предположение “оптимист(Денис)” — истинно.

Рассмотрим процесс получения графа вывода методом опровержения с помощью резо­люций, используя следующий пример.

Пусть множество формул

G={G_i} : G₁ : "X$Y(ùP(X)®Q(Y));

G₂ : "Z(P(a)®R(Z))

и требуется доказать следствие Н :

H : ùR(b)®$UQ(U).

Преобразовав эти формулы в предложения, указывая знаком отрицания следствие, получим множество предложений:

{P(X)ÚQ(f(X)), ùP(a)ÚR(Z), ùR(b), ùQ(U)} —

невыполнимость которых требуется доказать.

Граф вывода методом опревержения для этих предложений представлен на рис. 9.1.

Подграф графа вывода, отображающий множество предложений, используемых для получения пустого предложения, называют графом опровержения(рис. 9.2). Таким образом, корнем графа опровержения является пустое предложение. Заметим, что в графе вывода может быть несколько пустых предложений и соответственно несколько графов опровержения.Графом поисканазывают подграф графа вывода, покрывающий граф опровержения.

P(X)ÚQ(f(X)) ùP(a)ÚR(Z) ùR(b) ùQ(U)

Q(f(a))ÚR(Z) P(X) ùP(a)

Q(f(a)) Q(f(a)) R(Z) R(Z)

Рис. 9.1. Граф вывода

Рис.9.2. Граф опровержения