Правила вывода

1) правило индивидуализаций (А4)

"xA(x) |® A(t), где t – свободны для x в А(х)

"x A(x) a A(x)

"x A(x) a A(в) – удаление конъюнкции

"x A(x) a A(f(x))

"x A(x) a A(y) – переименование

2) правило существования (Е₄ - Мендельсон)

A(t) a $x A(x)

частный случай

A(x) a $x A(x)

A(в) a $x A(x) – введение дизъюнкции

A(f(x)) a $x A(x)

A(y) a $x A(x)

3) Правило обобщения (Generalization)

A(x) a "x A(x)

4) Правило выбора С(choice) С-правило

$x A(x)a A(в)

5) Правило вывода (МП правило)

Определение: Формула В выводима в логике предикатов (aВ), если может быть построена цепочка формул: В₁... В либо аксиома, либо применение правило.

Пример: Доказать, что выводимо

a "x, "x₂ A® "x₂"x₁A

1) "x"x₂A (гипотеза);

2) "x₂А (правило А4);

3) А (правило A4);

4) "x₁A (Gen);

5) "x₂"x₁A (Gen).

Теорема: Если в исчислений предикатов в выводимо (a), то В – общезначимо.

Утверждение Геделя: если формула В общезначима, то она является теоремой (т.е. она выводима: aВ).

Утверждение о непротиворечивости: не выводимо А и ùА одновременно.

Определение: Формула В выводима (aВ) из гипотез Г=F_­1,F₂,... F_m.

Г a В, если существует последовательность формул, которые получены из гипотез с применением аксиом и правил вывода.

Пример: $x (p(x) ® q(x)), "x p(x) a $x q(x)

1) $x (p(x) ® q(x) (гипотеза);

2) Vx p(x) (гипотеза);

3) р(а) ® q(a) (С-правило);

4) р(а) (А_­4­,2);

5) q(a) (МП – правило 3,4®5);

6) $х q(x) (Е_­4­).

Теорема: Формула В – логическое следствие из гипотез Г=F_­1­,F_­2­…F_­m­ тогда и только тогда, когда в любой интерпретации I конъюнкция F_­1­&F_­2­&…&F_­m­®B - тавтология (общезначимость формулы).

Гипотезы формулируются, преобразуются в ПНФи после этого проверяется общезначимость.
Пример:

" x(p(x))®q(x)

p(a)

q(a)

1. интерпретации

(ùl_­2­(i)Úl_­2­(i))&l_­2­(a)®l_­2­(a)

(`aÚA)(`bÚB)…(`dÚD)&a®A

aA(`bÚB)…(`dÚD)®A – тавтология (УК)

2. прямая волна

1) "x (p(x))®q(x) – гипотеза;

2) p(x)®q(x) – А_­4­(конкретизация);

3) $x (p(x)-q(x)) – правило существования Е_­4­;

4) p(a)®q(a) – С-правило к 3);

5) p(a) – гипотеза;

6) q(a) - МП-правило(4,5®6)

Данный метод неэффективен.

Теорема: Формула В – логическое следствие из гипотез Г=F_­1­,F_­2­…F_­m­_­­,если F_­1­&F_­2­&…&F_­m­&B противоречиво.

В частном случае Г=1, ùВ противоречиво,тогда В – выводимо (aВ).

Метод Дэвиса – Патнема можно применить, если исключить кванторы. Пусть формула находитсся в ПНФ Kx₁,Kx₂,... Kx_n­М(x_­1­…x_­n­)

1). Если Kx₁­ (первый слева квантор,не предшествующий квантору всеобщности $x_i),то можно применить С-правило, которое позволяетустранить (вычеркнуть, элиминировать) вместо всех вхождений переменной x_­1­ подставляется произволная постоянная из области интерпретации

$ x(p(x)®q(x))ap(a)®q(a)

2). Если квантору существования предшествует n кванторов всеобщности, то вместо соответствующей переменной x_­n+1­ подставляется функция f(x_­1­…x_­n), после этого квантор $ элиминируется

" x_­1­" x_­2­…" x_­n­ $ x_­­_­n+1­ x_­n+1­ M(x_­1­…x_­n+1)

n f(x_­1­,x_­2­…x_­n)

f(x_­1­,x_­2­…x_­n) – Сколемовская функция (Scolem).

Обоснование: если квантор $ находится в области действия кванторов ", то после устранения квантора существования значение этой переменной зависит от значения предшествующих переменных с кванторами " и эта функциональная. После устранения кванторов $ формула называется Сколемовской Стандартной Формой.

Пример:

$x "y "z $u "v $w p(x,y,z,u,v,w)

a f(y,z) g(y,z,v)

По правилу А4 можно исключить все кванторы $ и прийти к Сколемовской Формуле без кванторов.

Матрица М приведена к КНФ и представляетс собой множество дизюнктов S.

Теорема: Формула F противоречива, если S противоречимо (невыполнимо),если существует вывод пустого дизъюнкта.

Правило Дэвиса – Патнема применимо к предикатам P(t_­1­…t_­n­) и P(l_­1­…l­_­n­), где t_­i ­и l_­i­ – термы, если существует унифицирующая подстановка аргументор предикатов, при которых однотипные предикаты совпадают.

Унификация – процедура выбора унифицирующей подстановки.

P(t_­1­…t_­n­), то {t_­1­/l_­1­…t_­i­/l_­i­}

P(l_­1­…l­_­n­) множество рассогласования

Для каждой пары подстановка возможна, если один из термов – переменная, если найдется такая переменная в одном из термов, которую можно заменить частью или полностью другим термом.

x/y x«y

x/a xa

x/f(y) xf(y)

x/f(x) xf(x)

После того, как подстановка найдена, она выполняется для всех вхождений переменной. Эту подстановку можно рассматривать как частичную интерпретацию. При если унификация возможна, то возможно применение правил Дэвиса – Патнема к соответствующим предикатам. Если унификация невозможна, то невозможна и интерпретация на любом интервале и вывод невозможен.

Порядок применения метода Дэвиса – Патнема.

1)привести формулы к ПКНФ;

2)привести формулы к Сколемовской Стандартной форме без кванторов;

3)применить правила Дэвиса – Патнема с использованием унификации.

Пример:

F_­1­:"x (c(x)®w(x)&r(x))

F_­2­: $x (c(x)&o(x))

G: $x(o(x)&r(x))

1) приводим к ПКНФ

F_­1­:"x (c(x)®w(x)&r(x))=>"(ùc(x)Úw(x)&(ùc(x)Úr(x))

F_­2­: $x(c(x)&o(x))ac(a)&o(a)

G: $x (o(x)&r(x))aù($x(o(x)&r(x))

ùc(x)Úw(x) ùc(a)Úw(a)"x(ùo(x)&r(x)) w(a)

ùc(x)Úr(x) ùc(a)Úr(a) r(a) c (противоречие,

c(a) c(a) ùr(a) невыполнимо)

ùo(x)Úùr(x) ùo(a)Úùr(a)

o(a) o(a)

Для формализации машинного вывода алгоритм Дэвиса – Патнема заменяется правилом резолюций.Уточнения:

1) приводится к ПКНФ;

2) приводится к Сколемовской форме;

3) правило резолюции к контрарным предикатам, если существует унификация.

Пример:

F_­1­:"x (c(x)®w(x)&r(x))

F_­2­: $x (c(x)&o(x))

G: $x(o(x)&r(x))

ùc(x)Úw(x) ùc(x)Úr(x) c(a) o(a) ùo(x)Úùr(x)

ùc(a)Úw(a) x=a

r(a) ùr(a)

Этот метод связан с перебором.