Пусть дан алфавит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 – формулы, то (F1); (F1 & F2); (F1 F2); (F1 F2); (F1 F2) также формулы;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.13. Исчисление предикатов. Правила записи сложных суждений.Рассмотренные лог. операции при использовании термов, предикатов и кванторов позволяют формировать внутреннюю структуру предложения и формировать сложные суждения.см. вопрос 3.1) за квантором общности чаще всего следует лог. связка импликации, а за квантором существования – конъюнкции;2) если формула содержит подформулу, то внутренняя формула не должна содержать кванторов, связывающих ту же переменную, что и квантор формулы;3) предикат и функция должны иметь одно и то же количество аргументов всюду в формуле;4) значения всех предметных переменных и постоянных должны принадлежать одной области определения предиката или функции;5) если в одной формуле есть кванторы общности и существования, то при формализации суждений следует стремиться поставить квантор существования слева всей формулы.14. Исчисление предикатов. Законы эквивалентных преобразований.Прежде всего в это множество входят все законы исчисления высказываний (см. вопрос 4), обеспечивающие преобразование формул при наличии кванторов общности и существования.Закон коммутативности справедлив только для одноимённых кванторов:xy(F2(x, y)) = yx(F2(x, y));xy(F2(x, y)) = yx(F2(x, y));но xy(F2(x, y)) ≠ yx(F2(x, y));xy(F2(x, y)) ≠ yx(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; …)15. Исчисление предикатов. Пренексная нормальная форма (ПНФ) формулы.Для облегчения анализа сложных суждений оказывается удобным приведение формулы алгебры предикатов к нормальной форме. В алгебре предикатов необходимо предварительно отделить кванторы от логических формул, т. е. сформировать кванторную и безкванторную части формулы (ПНФ). В последующем бескванторную часть формулы можно преобразовать к КНФ или ДНФ формулы.Суть предварительного преобразования формулы к виду ПНФ состоит в том, что все кванторы формулы выносят влево, используя законы алгебры предикатов. В результате этих алгебраических преобразований может быть получена формула вида: F = >|x1>|x2…>|xn(M), где >|xi - кванторы существования или общности, т. е. >| {; }, а M – безкванторная часть формулы. Часть формулы >|x1>|x2…>|xn называют префиксом ПНФ, а M – матрицей ПНФ.Алгоритм преобразования формулы к виду ПНФ:1) Исключить всюду логические связки и по правилам эквивалентных преобразований.2) Продвинуть отрицание до атомарной формы по закону де Моргана.3) Переименовать связанные переменные по правилу: “найти самое левое вхождение предметной переменной такое, что это вхождение связано некоторым квантором, но существует ещё одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной”, операцию повторять пока возможна замена связанных переменных.4) Вынести кванторы влево согласно закону дистрибутивности и по аксиомам лог. связки двух формул, одна из которых не содержит свободной переменной, связанной в другой формуле каким-либо квантором.16. Исчисление предикатов. Сколемовская стандартная форма формулы.Наличие разноимённых кванторов усложняет анализ суждений. Поэтому можно рассмотреть более узкий класс формул, содержащий только кванторы общности, т. е.F = x1x2…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 = x1x2…xn(D1 & D2 & …), называют сколемовской стандартной формой формулы. В этой формуле Di – дизъюнкты, xi – предметные переменные. Каждый член дизъюнкта называют литерой.