4.2.2.1. Правила подстановки

Если в формулу F(х), содержащую свободную переменную x, выполнить всюду подстановку вместо x терма t , то получим формулу F(t).

Этот факт записывают так:

x  ^t F(x)

F(t).

Подстановка называется правильной, если в формуле всюду вместо свободной переменной x выполнена подстановка терма t..

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

Например,

_x1^x2x₃(P₁(x₁, x₃)P₂(x₂))

x₃(P₁(x₂, x₃)P₂(x₂)).

Это - правильная подстановка, так как x₁ –свободная переменная.

_x1^{f(x2, t)} x₃(P₁(x₁, x₃) P₂(x₂))

x₃(P₁(f(x₂, t), x₃) P₂(x₂)).

Это - правильная подстановка, так как x₁ –свободная переменная.

. _x3^x2x₃(P₁(x₁, x₃) P₂(x₂))

x₃(P₁(x₁, x₂) P₂(x₂)).

Это - неправильная подстановка, т.к. x₃ –связанная _x3.

_x2^x3x₃(P₁(x₁, x₃) P₂(x₂))

x₃(P₁(x₁, x₃) P₂(x₃)).

Это - неправильная подстановка, т.к. предикат P₂(x₃) попадает в область действия квантора x₃.

Если матрица ПНФ или ССФ не содержит сколемовских функций, то для вывода заключения применим принцип резолюции исчисления высказываний.

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

Например, если даны два дизъюнкта (P₁(x)P₂(x)) и (P₁(f(x))P₃(y)), то для получения контрарной пары атомов возможна подстановка:

_x^f(х)(P₁(x)P₂(x))

(P₁(f(x))P₂(f(x))).

В результате склеивания дизъюнктов может быть получена резольвента: (P₁(f(x))P₂(f(x)))(P₁(f(x))P₃(y))=(P₂(f(x)) P₃(y)).

Если пара дизъюнктов имеет вид (P₁(f₁(x))P₂(x)) и (P₁(f₂(x))P₃(y)), то никакая подстановка не позволит сформировать резольвенту.

Пример: даны две формулы P₃(a; x; f(q(y))) и P₃(z; f(z); f(u)).

Выполнить унификацию контрарных атомов.

_z^a P₃(z; f(z); f(u)) _x ^f(a) P₃(a; x; f(q(y))) _u^q(y) P₃(a; f(a); f(u))

P₃(a; f(a); f(u)); P₃(a; f(a); f(q(y))); P₃(a; f(a); f(q(y))).

В результате получены два контрарных атома:

P₃(a; f(a); f(q(y))) и P₃(a; f(a); f(q(y))).

Пример: даны две формулы P₃(x; a; f(q(a))) и P₃(z; y; f(u)).

Выполнить унификацию контрарных формул.

_x^bP₃(x; a; f(q(a))) _y^aP₃(z; y; f(u))

P₃(b; a; f(q(a))); P₃(z; a; f(u));

_z^b P₃(z; a; f(u))

P₃(b; a; f(u));

_u^q(a)P₃(b; a; f(u))

P₃(b; a; f(q(a))).

В результате получены две контрарных формулы:

P₃(b; a; f(q(a))) и P₃(b; a; f(q(a))).

4.2.2.2. Правила введения и удаления кванторов

П1. Если дана формула (F₁(t)F₂(x)) и F₁(t) не содержит свободной переменной x, то формула (F₁(t)x(F₂(x))) выводима в исчислении предикатов, т.е.

(F₁(t) F₂(x))

(F₁(t) _x(F₂(x))).

П2. Удаление квантора всеобщности

_x(F(x))

F (t).

П3. Введение квантора существования

F(t)

_x(F(x)).

П4. Удаление квантора существования

_x(F(x))

F(a).

П5. Смена квантора:

 _x(F(x)) _x(F(x))

_x(F(x)), _x(F(x)).

П6. Перенос квантора, если t не содержит переменной x:

_x(F₁(x)) F₂(t) _x(F₁(x))F₂(t)

_x(F₁(x) F₂(t)), _x(F₁(x) F₂(t)), где _x{_x,_x},

F ₁(t) _x(F₂(x)) _x(P(x))F(t) _x(P(x))F(t)

_x(F₁(t)F₂(x)), _x(P(x)F(t)), _x(P(x)F(t)).

П7. Введение новой переменной:

_x(F₁(x))_x(F₂(x)) _x(F₁(x))_x( F₂(x))

_y_x(F₁(y) F₂(x)), _y_x(F₁(y) F₂(x)).

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