Исчисление предикатов. Алгебра предикатов. Основные логические операции.

Пусть дан алфавитT = T1  T2  T3  T4  T5  T6  T7, гдеT1 = {x; y; z; …} – предметные переменные;T2 = {a; b; c; …} – предметные постоянные;T3 = {, &, , , } – лог. связки;T4 = {f1i; f2j; f3k; …} – функциональные символы;T5 = {P1i; P2j; P3k; …} – предикатные символы;T6 = {; } – кванторы;T7 = {;; (; )} – вспомогательные символы. Функциональные символы определяют функциональные отношения между предметными переменными и предметными постоянными и формируют термы по правилу: 1) всякая предметная переменная и предметная постоянная есть терм; 2) если fin – n-местный функциональный символ и t1, t2, … tn – термы, то fin(t1, t2, … tn) также есть терм; 3) никаких других термов нет. Предикатные символы, применённые к термам, порождают элементарные формулы по правилу: если Pin – предикатный символ и t1, t2, … tn – термы, то Pin(t1, t2, … tn) – элементарная формула. Обычные формулы исчисления предикатов определяются по правилу: 1) всякая элементарная формула есть формула, т. е. Fi = Pin(t1, t2, … tn); 2) если F1 и F2 – формулы, то (F 1); (F1 & F 2); (F1  F 2); (F1  F 2); (F1  F 2) также формулы; 3) если F – формула, а x – предметная переменная, то x(F) и x(F) также формулы; 4) никаких других формул нет. Всякая формула, содержащая только предметные постоянные, есть формула исчисления высказываний. Простейшими логическими операциями над предикатами являются отрицание, конъюнкция, дизъюнкция, импликация и эквиваленция. Использование этих логических связок не определяет связывания предметных переменных. Отрицание (F(t1, t2, … tn)) – одноместная операция, посредством которой из данной формулы F(t1, t2, … tn) получают её отрицание. Конъюнкция (F1(t11, t12, … t1n) & F2(t21, t22, … t2n)) есть двухместная операция, посредством которой из двух формул F1 и F2 получают новую формулу F(t11, t12, … t1n, t21, t22, … t2n) = F1 & F2 с числом предметных переменных и постоянных, равным их объединению у исходных формул. Полученная формула имеет значение true т. и только т., когда обе исходные формулы F1 и F2 имеют значение true. Дизъюнкция (F1(t11, t12, … t1n)  F2(t21, t22, … t2n)) есть двухместная операция, посредством которой из двух формул F1 и F2 получают новую формулу F(t11, t12, … t1n, t21, t22, … t2n) = F1  F2 с числом предметных переменных и постоянных, равным их объединению у исходных формул. Полученная формула имеет значение true т. и только т., когда хотя бы одна из исходных формул имеет значение true. Импликация (F1(t11, t12, … t1n)  F2(t21, t22, … t2n)) есть двухместная операция, посредством которой из двух формул F1 и F2 получают новую формулу F(t11, t12, … t1n, t21, t22, … t2n) = F1  F2 с числом предметных переменных и постоянных, равным их объединению у исходных формул. Полученная формула имеет значение false т. и только т., когда F1 имеет значение true, а F2 – false. Эквиваленция (F1(t11, t12, … t1n)  F2(t21, t22, … t2n)) есть двухместная операция, посредством которой из двух формул F1 и F2 получают новую формулу F(t11, t12, … t1n, t21, t22, … t2n) = F1  F2 с числом предметных переменных и постоянных, равным их объединению у исходных формул. Полученная формула имеет значение true т. и только т., когда обе формулы F1 и F2 имеют одно и то же значение true или false. 1 3) Исчисление предикатов. Правила записи сложных суждений. Рассмотренные лог. операции при использовании термов, предикатов и кванторов позволяют формировать внутреннюю структуру предложения и формировать сложные суждения. см. вопрос 3)1) за квантором общности чаще всего следует лог. связка импликации, а за квантором существования – конъюнкции; 2) если формула содержит подформулу, то внутренняя формула не должна содержать кванторов, связывающих ту же переменную, что и квантор формулы; 3) предикат и функция должны иметь одно и то же количество аргументов всюду в формуле; 4) значения всех предметных переменных и постоянных должны принадлежать одной области определения предиката или функции; 5) если в одной формуле есть кванторы общности и существования, то при формализации суждений следует стремиться поставить квантор существования слева всей формулы. 1 4) Исчисление предикатов. Законы эквивалентных преобразований. Прежде всего в это множество входят все законы исчисления высказываний (см. вопрос 4), обеспечивающие преобразование формул при наличии кванторов общности и существования. Закон коммутативности справедлив только для одноимённых кванторов:xy(F2(x, y)) = yx(F2(x, y));xy(F2(x, y)) = yx(F2(x, y));но xy(F2(x, y)) ≠ yx(F2(x, y));xy(F2(x, y)) ≠ yx(F2(x, y));Перестановка разноимённых кванторов недопустима. Закон дистрибутивности существенно зависит от имени квантора и типа логической связки:x(F1(x)) & x(F2(x)) = x(F1(x) & F2(x));x(F1(x))  x(F2(x)) = x(F1(x)  F2(x));но x(F1(x))  x(F2(x)) ≠ x(F1(x)  F2(x));x(F1(x)) & x(F2(x)) ≠ x(F1(x) & F2(x));Закон де Моргана определяет двойственные преобразования формул при наличии кванторов:x(F(x)) = x(F(x))x(F(x)) = x(F(x))В алгебре предикатов, как и в алгебре высказываний, логические связки упорядочены по силе и первоочерёдности исполнения следующим порядком: ; & ; ; . Вспомогательные символы в исчислении предикатов имеют то же значение, что в исчислении высказываний. Если формула алгебры предикатов F имеет вхождением подформулу Fi, т. е. F(t1; t2; … Fi; …), для которой существует эквивалентная её подформула Fj, т. е. Fi  Fj, то возможна подстановка в формулу F всюду подформулы Fj вместо формулы Fi без нарушения истинности формулы:F(t1; t2; … Fi; …) = F(t1; t2; … Fj; …)1 5) Исчисление предикатов. Пренексная нормальная форма (ПНФ) формулы. Для облегчения анализа сложных суждений оказывается удобным приведение формулы алгебры предикатов к нормальной форме. В алгебре предикатов необходимо предварительно отделить кванторы от логических формул, т. е. сформировать кванторную и безкванторную части формулы (ПНФ). В последующем бескванторную часть формулы можно преобразовать к КНФ или ДНФ формулы. Суть предварительного преобразования формулы к виду ПНФ состоит в том, что все кванторы формулы выносят влево, используя законы алгебры предикатов. В результате этих алгебраических преобразований может быть получена формула вида: F = >|x1>|x2…>|xn(M), где >|xi - кванторы существования или общности, т. е. >|  {; }, а M – безкванторная часть формулы. Часть формулы >|x1>|x2…>|xn называют префиксом ПНФ, а M – матрицей ПНФ. Алгоритм преобразования формулы к виду ПНФ: 1) Исключить всюду логические связки  и  по правилам эквивалентных преобразований. 2) Продвинуть отрицание до атомарной формы по закону де Моргана. 3) Переименовать связанные переменные по правилу: “найти самое левое вхождение предметной переменной такое, что это вхождение связано некоторым квантором, но существует ещё одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной”, операцию повторять пока возможна замена связанных переменных. 4) Вынести кванторы влево согласно закону дистрибутивности и по аксиомам лог. связки двух формул, одна из которых не содержит свободной переменной, связанной в другой формуле каким-либо квантором. 1 6) Исчисление предикатов. Сколемовская стандартная форма формулы. Наличие разноимённых кванторов усложняет анализ суждений. Поэтому можно рассмотреть более узкий класс формул, содержащий только кванторы общности, т. е. F = x1x2…xn(M)Для устранения кванторов существования разработан алгоритм Сколема, вводящий сколемовскую функцию для связи предметной переменной квантора существования с другими предметными переменными. Алгоритм Сколема: 1) представить формулу F в виде ПНФ; 2) найти наименьший индекс i квантора существования такой, что все предшествующие в префиксе кванторы есть кванторы общности:a) если i = 1, т. е. квантор xi находится на первом месте префикса, то вместо переменной, связанной квантором существования, подставить всюду предметную постоянную ai, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования вычеркнуть в префиксе;b) если i > 1, т. е. квантор xi находится не на первом месте префикса, а перед квантором существования стоит часть префикса, состоящая только из кванторов общности, то выбрать (i – 1)-местный функциональный символ, отличный от функциональных символов матрицы M и выполнить замену предметной переменной xi, связанной квантором существования на функцию f(x1; x2; … xn) и квантор существования вычеркнуть в префиксе;c) найти следующий индекс квантора существования и перейти к исполнению шага 2. Если таких индексов нет, то конец. Бескванторную часть формулы теперь можно преобразовать а виду КНФ или ДНФ. Чаще всего требуется выполнить преобразование к виду КНФ для логического вывода по принципу резолюции. Формулу, полученную в результате введения сколемовской функции и преобразованную в КНФ, т. е. F = x1x2…xn(D1 & D2 & …), называют сколемовской стандартной формой формулы. В этой формуле Di – дизъюнкты, xi – предметные переменные. Каждый член дизъюнкта называют литерой.