Файл: Основные положения исчислений Учебные вопросы.pptx

Предикат (лат. praedicatum «сказанное») в логике и лингвистике — сказуемое суждения, то, что высказывается (утверждается или отрицается) о субъекте. Предикат находится с субъектом в предикативном отношении и показывает наличие (отсутствие) у предмета некоторого признака.

Предикаты могут принадлежать к следующим семантическим типам:

таксономические — классифицируют предмет, например «Это животное — кошка»;
реляционные — указывают отношение объекта к другим. Пример: «Авраам — отец Исаака»;
характеризующие — указывают на постоянные, временные, динамические и т. п. признаки объекта.

Определение предиката

Классификация предикатов

Интерпретация предикатов

Логические операции над предикатами

Операции связывания предикатов

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

Пример 1: «Всякий человек смертен» - х (Человек(х)  Смертен(х))

Пример 2: «Всякий студент изучает какую-нибудь предмет» - х (Студент(х)  у Наука(у)&Изучает(х,у))

Пример 3: «Квадрат любого четного числа больше 1»- х(Четное_число(х)>(Квадрат(х),1)).

Типы суждений (высказываний)

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

Законы алгебры предикатов

Имя закона	Равносильные формулы
Коммутативности	∀x∀y(F(x, y))≡∀y∀x(F(x, y)) ∃x∃y(F(x, y))≡∃y∃x(F(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(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))≡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)) ∀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))

Примеры использования кванторов

3.2. Определение формальной системы предикатов первого порядка

Алфавит формальной системы Исчисление предикатов

Алфавит формальной системы.

x1, x2, …, xn, … – предметные переменные;
a1, a2, …, an, … – предметные константы;
A11, A22, …, Alm, P11,… – предикатные буквы;
f11, f22, …, flk,… – функциональные буквы.

В логике предикатов существует понятие терма:

Любую предметную переменную и предметную постоянную предиката называют термом - ti.
Если fi - функциональный символ и t1,t2,..., tn – его аргументы-термы, то fi(t1,t2,…,tn) также есть терм.
Никаких иных термов нет.

Формулы формальной системы

Введем понятие формулы в исчислении предикатов:

Если Pi – предикатный символ и t1,t2,...,tn – термы, то F=Pi(t1,t2,...,tn ) - элементарная формула.
Если F1 и F2 - формулы, то ¬F1, ¬F2, (F1&F2), (F1∨F2), (F1→F2), (F1↔F2) - также формулы.
Если F - формула, a x - предметная переменная, входящая в формулу F, то ∀x(F) и ∃x(F) - также формулы.
Никаких иных формул нет.

Аксиомы исчисления предикатов

Правила вывода

Правила для кванторов

Правила преобразования формул

3.3. Метод резолюции

Предваренная нормальная форма формулы исчисления предикатов

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

Алгоритм приведения к предваренной нормальной форме

Пример приведения к предваренной нормальной форме

Преобразовать формулу:

∀x(P(x) & ∀y¬∃x(¬ Q(x, y) → ∀y (R(a, x, y))) )

Шаг 1. Исключим импликацию

∀x(P(x) & ∀y ¬∃x ((Q(x, y)  ∀y R(a, x, y)))

Шаг 2. Перенесем отрицание

∀x(P(x) & ∀y ∀ x (¬(Q(x, y)  ∀y R(a, x, y))) = ∀x(P(x) & ∀y ∀ x (¬Q(x, y) &¬ ∀y (R(a, x, y)))= ∀x(P(x) & ∀y ∀ x (¬Q(x, y) &∃y (¬ R(a, x, y))) )

Шаг 3.Переименуем связанную переменную x=t, y=q

∀x(P(x) & ∀y ∀ t (¬Q(t, y) & ∃q¬R(a, t, q)))

Перенесем кванторы влево

∀x ∀ y∀t ∃q (P(x) & (¬Q(t, y) & ¬ R(a, t, q)).

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

Шаг 1: представить формулу F в виде ПНФ, т. е. F=ℜx1ℜx2…ℜxn(M), где ℜi∈{∀, ∃}, а М=D1&D2&D3&…,
Шаг 2: найти в префиксе самый левый квантор существования и заменить его по правилу:
a) если квантор существования находится на первом месте префикса, то вместо переменной, связанной этим квантором, подставить в матрице всюду предметную постоянную, отличную от встречающихся постоянных, а квантор существования удалить,
b) если квантор существования находится на i-м месте префикса, т.е.∀x1∀x2…∀xi-1∃xi ..., то выбрать (i-1)- местную сколемовскую функцию f(x1, x2,..xi-1), отличную от функций матрицы М, и выполнить замену предметной переменной xi, связанной квантором существования, на функцию f(x1, x2,..., xi-1), а квантор существования из префикса удалить.
Шаг 3: найти в префиксе следующий слева квантор существования и перейти к исполнению шага 2, иначе конец.
Формулу ПНФ, полученную в результате введения сколемовских функций, называют сколемовской стандартной формой (ССФ). Преобразованная таким образом матрица может быть допущена к анализу истинности суждения по принципу резолюции