Вопрос 40: Исчисление предикатов. Правила вывода на основе исчисления предикатов.

Алфавит исчисления предикатов включает в себя:

1. знаки пунктуации: {},();

2. логические (пропозициональные) связки множеств: $\lnot, \wedge, \vee, \to, \leftrightarrow$

3. кванторы: $\forall, \exists$

4. переменные: $x_k, k = 1,2;$

5. n -местные функциональные буквы (символы) $f_k^n, \text{где} \: k \geq 1, n \geq 0;$

6. n -местные предикатные символы $P_k^n, \text{где} \: k \geq 1, n \geq 0.$

Обычно для упрощения знаний при обозначении переменных вместо $x_ k$, используются символы w, v, w, х, у, z,... .

При обозначении констант обычно используются a, b, с, d,...; для функцииoнaльныx букв - вместо $f_k^n \: \text{для} \: n \neq 0$ используются f, g, h.

При обозначении предикатных символов применяются буквы латинского алфавита P, Q, R, S. Из символов алфавита можно строить различные выражения.

Любой символ переменной или константной буквы называется термом. Если $t_1,... t_n, n \geq 1$ - термы, то $f_k^n(t_1,... t_n)$ тоже = терм. Если $P_k^n$ - предикатная буква, а $t_1,... t_n$ - термы, то $P_k^n(t_1,... t_n)$ - элементарная формула, или атом. Если А и В - правильно построенные формулы (ППФ), то $\lnot A$, В, $A \wedge B$, $A \vee B$, $A \to B$, $A \leftrightarrow B$ тоже ППФ. Если А - ППФ, а х - переменная, то ($\forall x$) А, ($\exists x$) А тоже ППФ и А называется областью действия кванторов $\forall$ и $\exists$.

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

Пример: $(\forall x)(Q(x, y) \to R(x))$, х — связанная переменная, у - свободная переменная.

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

Пример: категорическое высказывание - $(\forall x)(P(x) \to S(x)$.

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

Интерпретация - любая система, состоящая из непустого множества ( $D \neq \varnothing$ ), называемого областью интерпретации, и какого-либо соответствия, относящего к каждой предикатной букве $P_k^n$ некоторое n-местное отношение в D, а каждой функциональной букве некоторую n-местную функцию, отображающую $D^n$ и $D$: $f_k^n: D^n \to D$.

При заданной интерпретации переменные «пробегают» область интерпретации D и всякой элементарной формуле присваивается значение True или False.

Если термы предикатной буквы, соответсгвующие элементам из системы D, удовлетворяют отношению, определенному данной интерпретацией, то значение элементарной формулы будет True, иначе - False.

Значение неэлементарной формулы вычисляется рекуррентно, исходя из значений составляющих ее формул в соответствии с таблицей истинности.

Для исчисления предикатов первого порядка не существует методов установления общезначимости любой формулы, т. е. исчисление предиката первого порядка неразрешимо. Однако если некоторая формула исчисления предикатов общезначима, то существуют процедуры для проверки её общезначимости, т. е. исчисление предикатов полуразрешимо.

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

К недостаткам данного подхода можно отнести следующие:

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

Моделью знаний в системах, основанных на исчислении предикатов, является описание решений задачи в виде множества утверждений, построенных на множестве базовых элементов с помощью синтаксических правил. Цель задачи также записывается в виде утверждения, справедливость которого нужно доказать или опровергнуть на основе существующих аксиом и семантических правил вывода. Одним из наиболее мощных средств вывода доказательств в настоящее время является метод резолюций.

Классические правила вывода:

1. Правило Modus Ponens: $\frac{A, A \to B}{B}$, читается так: если A – выводима и A влечет B, то B – выводимая формула.
2. Цепное правило: $\frac{A \to B, B \to C}{A \to C}$, читается так: если формулы $A \to B$ и $B \to C$ выводимы, то выводима и формула $A \to C$.
3. Правило подстановки: если формула A(x) выводима, то выводима и формула A(B), в которой все вхождения литерала x заменены формулой B.
4. Правило резолюций: если выводимы формулы двух дизьюнктов, имеющих контрарную пару, $A \vee c$ и $B \vee \lnot c$, то выводима формула дизьюнкта $A \vee B$, полученного из данных двух удалением контрарной пары.