Сколемовская стандартная форма формулы

Наличие разноимен­ных кванторов усложняет вывод заключения. Для устранения кванторов существования в ПНФ и представления ее в виде F = "_x1"_x2 ¼"_xn (M) разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с предметными переменными кванторов всеобщности.

Алгоритм приведения формулы к виду ССФ:

Шаг 1: представить формулу Fв виде ПНФ, т.е.

F =Âx₁Âx₂¼Âx_n(M), где Â_iÎ{"; $};

Шаг 2: найти в префиксе самый левый квантор существования:

a) если квантор находится на первом месте префикса, то вместо переменной, связанной кван­тором существования, подставить всюду предметную по­стоянную a, отличную от встречающихся постоянных в матрице формулы, а квантор существования удалить;

b) если квантор находится не на первом месте префикса, т.е. "_x1"_x2¼"_xi-1$_xi .., то выбрать (i-1)-местный функциональный символ, отлич­ный от функциональных символов матрицы М и выполнить замену предметной переменной x_i, связанной кванто­ром существования, на функцию f(x₁, x₂,..x_i-1) и квантор существования удалить.

Шаг 3: найти следующий справа квантор существования и перей­ти к исполнению шага 2, иначе конец.

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

Пример: F=$_x1"_x2"_x3$_x4"_x5$_x6((P₁(x₁, x₂)ÚùP₂(x₃, x₄, x₅))&P₃(x₄, x₆)).

· заменить предметную переменную x₁ на постоянную a:

F="_x2"_x3$_x4"_x5$_x6 ((P₁. (a, x₂)ÚùP₂.(x₃, x₄, x₅))&P₃ (x₄, x₆));

· заменить предметную переменную x₄ на функцию f ₁.(x₂, x₃):

F="_x2"_x3"_x5$_x6 ((P₁.(a, x₂)ÚùP₂ (x₃, f₁(x₂, x₃), x₅))&P₃ (f₁(x₂, x₃), x₆));

· заменить предметную переменную x₆ на функцию f₂(x₂, x₃, x₅):

F="_x2"_x3"_x5((P₁(a, x₂)ÚùP₂(x₃, f₁(x₂, x₃), x₅))&P₃(f₁(x₂, x₃),

f₂(x₂, x₃, x₅))).

Множество дизъюнктов матрицы:

К={(P₁(a, x₂)ÚùP₂(x₃, f₁(x₂, x₃), x₅)); P₃(f₁(x₂, x₃), f₂(x₂, x₃, x₅))}.

 

Пример: F=$_z"_w$_x"_y((P₁ z)ÚP₂ (х)ÚP₃.(y))&(ùP₂ (w)ÚP₂ (х)ÚP₃.(y))& (ùP₂ (w)ÚùP₁ (z)ÚP₃.(y))).

· заменить предметную переменную z на постоянную a и удалить квантор $_z:

F="_w$_x"_y((P₁ (a)ÚP₂ (х)ÚP₃.(y))&(ùP₂ (w)ÚP₂ (х)ÚP₃.(y))& (ùP₂ (w)ÚùP₁ (a)ÚP₃.(y))).

· заменить предметную переменную x на функцию f(w) и удалить квантор $_x:

F="_w"_y((P₁ (a)ÚP₂ (f(w))ÚP₃.(y))&(ùP₂ (w)ÚP₂ (f(w))ÚP₃.(y))& (ùP₂ (w)Ú

ùP₁ (a)ÚP₃.(y))).

 

· заменить предметную переменную x₆ на функцию f₂(x₂, x₃, x₅):

F="_x2"_x3"_x5((P₁(a, x₂)ÚùP₂(x₃, f₁(x₂, x₃), x₅))&P₃(f₁(x₂, x₃),

f₂(x₂, x₃, x₅))).

Множество дизъюнктов матрицы:

К={(P₁(a, x₂)ÚùP₂(x₃, f₁(x₂, x₃), x₅)); P₃(f₁(x₂, x₃), f₂(x₂, x₃, x₅))}.

 

Пример: F=$_z"_w$_x"_y((P₁ z)ÚP₂ (х)ÚP₃.(y))&(ùP₂ (w)ÚP₂ (х)ÚP₃.(y))& (ùP₂ (w)ÚùP₁ (z)ÚP₃.(y))).

· заменить предметную переменную z на постоянную a и удалить квантор $_z:

F="_w$_x"_y((P₁ (a)ÚP₂ (х)ÚP₃.(y))&(ùP₂ (w)ÚP₂ (х)ÚP₃.(y))& (ùP₂ (w)ÚùP₁ (a)ÚP₃.(y))).

· заменить предметную переменную x на функцию f(w) и удалить квантор $_x:

F="_w"_y((P₁ (a)ÚP₂ (f(w))ÚP₃.(y))&(ùP₂ (w)ÚP₂ (f(w))ÚP₃.(y))& (ùP₂ (w)Ú

ùP₁ (a)ÚP₃.(y))).

Исчисление предикатов

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

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

Под интерпретацией формул следует понимать систему, состоящую из не­пустого множества V, называемого универсумом, и отображения предиката P(t₁,t₂,¼ t_n) на двухэлементное множество {и; л}. Предметные постоянные t_i и функциональные символы f_i(t₁, t₂,...) есть элементы tÎV, а предметные переменные есть обычные переменные, заданные на универсуме. Символы логических и кванторных операций приобретают также обычный смысл. Тогда каждому предикату P(t₁,t₂,¼ t_n), принявшему значение “и” или “л”, ставится в соот­ветствие n-местное отношение на множестве V.

Например, если V есть множество целых чисел, то в формуле

$x$y$z(P(x;+(y, z))):= “существует число x, которое меньше суммы чисел y и z" при х=5, у=1, z=3 имеем двухместную операцию +(1, 3) и двухместное отношение между числом 5 и значением операции +(1,3)=4. Отображение P(5;4) на двухэлементное множество дает значение “л”. При х=5, у=2, z=4 имеем +(2,4)=6 и P(5; 6)=”и”.

Другими словами, интерпретация функциональных символов опре­деляется по значениям функции на универсуме, а интерпретация предикатных символов по отображению на множество {и; л}.

Выделяют три класса формул: тождест­венно истинные, тождественно ложные и выводимые.

Тождественно истинные формулы - это особый класс формул, которые принимают значение “истины” для всех интерпретаций предметных постоянных, функциональных и предикатных символов; это - аксиомы исчисления предикатов.

Например, формула $x(F(x))«ù"x(ùF(x)):= формула ”существуют x, для которых F(x)=и”, эквивалентна формуле “не для всех x F(x)=л””. Это тождественно истинная формула.

Тождественно ложные формулы - это особый класс формул исчисления предикатов, которые принимают значение “ложь” для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула $_x(F(x))&"_x(ùF(x)):=“существуют x, для которых формула F(x)=и, и для всех x формула F(x)=л” является тождественно ложной.

Выполнимые формулы - это особый класс формул исчисления преди­катов, которые принимают значение “истина” не для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула $_x(F(x))®ù"_x(F(x)):=” если существует x, для которого F(x)=и, то не для всех х универсума F(x)=и”.

Вывод заключения из множества посылок есть:

F₁;F₂;¼F_n|¾ B,

где слева от знака “|¾” записывают множество посылок и необходимых аксиом F₁;F₂;¼F_n, а справа – заключение B.

Другая форма записи вывода заключения:

F₁; F₂;¼F_n

B,

где над чертой записывают множество посылок и аксиом F₁;F₂;¼F_n, а под чертой - заключение B.

Логический вывод заключения есть теорема:

|¾F₁&F₂&¼&F_n®B,

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

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

Если в формулу 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))).

 

⇐ Предыдущая17181920212223242526Следующая ⇒

Поделиться:

Воспользуйтесь поиском по сайту: