Практика по предикатному дедуктивному выводу

Метод дедуктивного вывода

Правила унификации предикатов

Если матрица ССФ не содержит сколемовских функций, то для вывода заключения применим принцип резолюции исчисления высказываний. Однако если аргументы атомов дизъюнктов ССФ содержат сколемовские функции, то для поиска контрарных атомов над дизъюнктами необходимо выполнять специальную операцию, называемую унификацией, - подстановку вместо предметных переменных аргумента атома новых предметных переменных, или предметных постоянных, или функциональных символов, т.е. термов, и получить новые формулы дизъюнктов, которые уже, возможно, допускают унификацию контрарных пар. В логике предикатов атомы являются контрарными, если соответствуют одному и тому же предикату с противоположными знаками и с одинаковыми аргументами. Множество подстановок при унификации дизъюнктов нужно выполнять последовательно, просматривая каждый раз только одну предметную переменную.

Рассмотрим примеры:

1. Выполнить унификацию дизъюнктов - контрарных атомов: P₃(a,x,f(q(y))) и ¬P₃(z,f(z),f(u)).

Решение представим схемой:

P₃(a,x,f(q(y))) ¬P₃(z,f(z),f(u))

Получены контрарные атомы: P₃(a,f(a),f(q(y))) и ¬P₃(a,f(a),f(q(y))).

2. Выполнить унификацию дизъюнктов – контрарных атомов: P₃(x,a,f(q(a))) и ¬P₃(z,y,f(u)).

Решение представим схемой:

P₃(x,a,f(q(a))) ¬P₃(z,y,f(u))

Получены контрарные атомы: P₃(b,a,f(q(a))) и ¬P₃(b,a,f((q(a))).

3. Выполнить унификацию дизъюнктов (P₁(x)∨¬P₂(x)) и (¬P₁(f(x))∨P₃(y)).

Решение:

Тогда в результате соединения дизъюнктов логической связкой «∨» может быть получена резольвента: (P₁(f(x))∨¬P₂(f(x)))∨(¬P₁(f(x))∨P₃(y)) =(¬P₂(f(x))∨ P₃(y)).

В логике предикатов вывод выполняется так же, как в исчислении высказываний. Все правила логики высказываний (ИВ) включены в множество правил логики предикатов (ИП).

1. Доказать истинность заключения в формуле:

Решение:

1. Введем обозначения для посылок:

F₁="_x(P₁(x)®ØP₂(x))

F₂="_x(P₃(x)®P₁(x))

2. Выполним по шагам дедуктивный вывод, вводя обозначения для получаемых формул:

F₃=(P₁(t)®ØP₂(t)) – по F₁ и правилу П1 и.п.[4],

F₄=(P₃(t)®P₁(t)) – по F₂ и правилу П1 и.п.,

F₅=(P₃(t)®ØP₂(t)) – по F₃ , F₄ и правилу П9 и.в.[5],

F₆="_x(P₃(x)®ØP₂(x)) – по F₅ и правилу П2 и.п.., ч.т.д.

Данному выводу соответствует граф:

2. Доказать истинность заключения в формуле:

Решение:

1. Введем обозначения для посылок:

F₁=∀_x(∃_y(P₁(x, y)&P₂(y))→∃_y(P₃(y)& P₄(x, y)))

F₂=¬∃_x(P₃(x))

2. Выполним по шагам дедуктивный вывод:

F₃=∀_x(¬P₃(x)) - по F₂ и закону отрицания,

F₄=¬P₃(t) - по F₃ и правилу П1 и.п.,

F₅=¬P₃(t)∨¬P₄(x, t) - по F₄ и правилу П3 и.в. при y=t (по правилам правильной подстановки и.п.),

F₆=∀_y(¬P₃(y)∨(¬P₄(x, y))) - по F₅ и правилу П2 и.п.,

F₇=¬∃_y(P₃(y)&P₄(x, y)) - по F₆ и правилам эквивалентных преобразований и де Моргана,

F₈=∃_y(P₁(t, y)&P₂(y))→∃_y(P₃(y)&P₄(t, y)) - по F₁ и правилу П1 и.п.,

F₉=¬∃_y(P₁(t, y)&P₂(y)) - пo F₇ и F₈ и правилу m.t.,

F₁₀=∀_y(¬P₁(t, y)∨¬P₂(y)) - по F₉ и правилам эквивалентных преобразований,

F₁₁=∀_y(P₁(t, y)→¬P₂(y)) - по F₁₀ и правилам эквивалентных преобразований,

F₁₂=∀_x∀_y(P₁(x, y)→¬P₂(y)) - по F₁₁ и правилу П2 и.п.,

F₁₃=¬∃_x(P₃(x))→∀_x∀_y(P₁(x, y)→¬P₂(y)) – по F₂ и F₁₂ и правилу П5 и.в., ч.т.д.

Данному выводу соответствует граф:

F₁="_x($_y(P₁(x,y)&P₂(y))®$_y(P₃(y)&P₄(x,y)))

F₂=Ø$_x(P₃(x))

F₈=$_y(P₁(t,y)&P₂(y))®$_y(P₃(y)&P₄(t,y))

F₃="_x(ØP₃(x))

П1 и.п.

по закону отрицания

F₄=ØP₃(t)

П1 и.п.

F₅=ØP₃(t)ÚØP₄(x,t)

П3 и.в.

F₆="_y(ØP₃(t)ÚØP₄(x,y))

П2 и.п.

F₇=Ø$_y(P₃(t)&ØP₄(x,y))

F₉=Ø$_y(P₁(t,y)& P₂(y))

m.t.

F₁₀="_y(ØP₁(t,y)ÚØ P₂(y))

F₁₁="_y(P₁(t,y)®Ø P₂(y))

F₁₂="_x"_y(P₁(x,y)®Ø P₂(y))

F₁₃=Ø$_x(P₃(x))®"_x"_y(P₁(x,y)®ØP₂(y))

П2 и.п.

П5 и.в.

3. Доказать истинность заключения в формуле:

Решение:

1. Введем обозначения для посылок:

F₁=∃_x(P₁(x)&∀_y(P₂(y)→P₄(x, y)))

F₂=∀_x(P₁(x)→∀_y(P₃(y)→¬P₄(x, y)))

2. Выполним по шагам дедуктивный вывод:

F₃=P₁(а)&∀_y(P₂(y)→P₄(a, y)) - по F₁ и правилу П3 и.п.,

F₄=P₁(a) - по F₃ и правилу П2 и.в.,

F₅=∀_y(P₂(y)→ P₄(a, y)) - пo F₃ и правилу П2 и.в.,

F₆=P₂(t)→ P₄(a, t) - по F₅ и правилу П1 и.п.,

F₇=P₁(t)→∀_y(P₃(y)→¬P₄ (t, y)) - по F₂ и правилу П1 и.п.,

F₈=∀_y(P₃(y)→¬P₄(a, y)) - по F₄ и F₇ при t=a по правилу m.p.,

F₉=P₃(t)→¬P₄(a, t) - по F₈ и правилу П1 и.п.,

F₁₀=P₄(a, t)→¬P₃(t) - по F₉ и правилу П6 и.в.,

F₁₁=P₂(t)→¬P₃(t) - по F₆ и F₁₀ и правилу П9 и.в.,

F₁₂=∀_x(P₂ (x)→¬P₃(x)) - по F₁₁ и правилу П2 и.п., ч.т.д.

∃_x(P₁(x)&∀_y(P₂(y)→P₄(x, y)))

∀_x(P₁(x)→∀_y(P₃(y)→¬P₄(x, y)))  

P₁(а)&∀_y(P₂(y)→P₄(a, y))

P₁(t)→∀_y(P₃(y)→¬P₄ (t, y))

∀_y(P₂(y)→ P₄(a, y))

P₁(a)

∀_y(P₃(y)→¬P₄(a, y))

∀_y(P₃(y)→¬P₄(a, y))

P₃(t)→¬P₄(a, t)

P₄(a, t)→¬P₃(t)

P₂(t)→ P₄(a, t)

P₂(t)→¬P₃(t)

∀_x(P₂ (x)→¬P₃(x))

П3 и.п.

П2 и.в.

П2 и.в.

П2 и.в.

П1 и.п.

П1 и.п.

m.p. при t=a

П1 и.п.

П6 и.в.

П9 и.в.

П2 и.п.

Данному выводу соответствует граф:

4. Дано высказывание: «Таможенные чиновники обыскивают каждого, кто въезжает в страну, кроме высокопоставленных лиц. Если некоторые люди способствуют провозу наркотиков, то на внутреннем рынке есть наркотик. Никто из высокопоставленных лиц не способствует провозу наркотиков. Следовательно, некоторые из таможенников способствуют провозу наркотиков». Правилен ли вывод?

Решение:

Пусть предметные переменные х и y определены на множестве индивидов. Введем предикаты:

P₁(x):=«быть таможенником»,

P₂(x,y):=«x обыскивает y»,

P₃(y):=«въезжать в страну»,

P₄(y):=«быть высокопоставленным лицом»,

P₅(y):=«способствовать провозу наркотиков».

Тогда формальная запись суждения имеет вид:

1. Введем обозначения для посылок:

F₁=∃_y(P₃(y)&P₅(y))

F₅=∀_y(P₃(y)&P₄(y)→¬P₅(y))

F₉=∀_y(P₃(y)&¬P₄(y)→∀_x(P₁(x)&P₂(x,y)))

2. Выполним по шагам дедуктивный вывод:

F₂=P₃(a)&P₅(a) - по F₁ и правилу П3 и.п.,

F₃= P₃(a) - по F₂ и правилу П2 и.в.,

F₄= P₅(a) - по F₂ и правилу П2 и.в.,

F₆=P₃(t)&P₄(t)→¬P₅(t) - по F₅ и правилу П1и.п.,

F₇=¬P₃(t)∨¬P₄(t)∨¬P₅(t) - по F₆,

F₈=¬P₄(a) - по F₇, F₃, F₄ при t=a, когда ¬P₃(а)=л и ¬P₅(а)=л,

F₁₀=∀_y∀_x(P₃(y)&¬P₄(y)→(P₁(x)&P₂(x,y))) –по F₉ и правилу П5 и.п.,

F₁₁=P₃(a)&¬P₄(a)→P₁(t)&P₂(t,a) - по F₁₀ при y=a и правилу П1 и.п.,

F₁₂= P₃(a)&¬P₄(a) - по F₃ и F₈ и правилу П1 и.в.,

F₁₃=(P₁(t)&P₂(t,a)) - по F₁₁ и F₁₂ и правилу m.p.,

F₁₄= P₁(t) - по F₁₃ и правилу П2 и.в.,

F₁₅= P₁(t)&P₅(t) - по F₄, F₁₄ при t=a и правилу П1 и.в.,

F₁₆=∃_x(P₁(x)&P₅(x)) - по F₁₅ и правилу П3 и.п., ч.т.д.

Данному выводу соответствует граф:

∃_y(P₃(y)&P₅(y))

∀_y(P₃(y)&P₄(y)→¬P₅(y))

P₃(a)&P₅(a)

P₃(t)&P₄(t)→¬P₅(t)

P₃(а)

P₅(a)

ØP₃(t)Ú¬P₄(t)ÚØP₅(t)

¬P₄(a)

P₁(t)&P₂(t,а)

P₁(t)

P₁(t)&P₅(t)

П1 и.п.

П2 и.в.

П1 и.п. при y=a

при t=a

П5 и.п.

m.p.

П1 и.в.

П2 и.в.

∀_y(P₃(y)&¬P₄(y)→∀_x(P₁(x)&P₂(x,y)))

П3 и.п.

∀_y"_х(P₃(y)&¬P₄(y)→(P₁(x)&P₂(x,y)))

P₃(a)&¬P₄(a)→P₁(t)&P₂(t,a)

P₃(a)&¬P₄(a)

П1 и.в. при t=a

$_х(P₁(х)&P₅(х))

П3 и.п.

Дата добавления: 2014-01-04