Общие понятия.

Формальная система F считается определенной, если:

1. Определен алфавит системы – счетное множество символов. Из алфавита образуется множество слов - некоторое подмножество всех цепочек из символов алфавита.
2. Определены формулы системы – некоторое подмножество слов. Как правило, определяется процедура составления формул из символов алфавита.
3. Определены аксиомы системы – некоторое подмножество формул.
4. Определены правила вывода системы – конечное множество отношений между формулами системы.

Логика предикатов – частный случай формальной системы.
Алфавит логики предикатов (или как ее еще называют, логики первого порядка) составляют:

1. Переменные.
2. Константы.
3. Функциональные символы.
4. Предикатные символы.
5. Константы Ложь и Истина.
6. Кванторы существования (обозначим СУЩ) и всеобщности (обозначим ВСЕ).
7. Логические связки отрицания (НЕ), конъюнкции(И), дизъюнкции (ИЛИ), импликации (->).
8. Символы скобок, точки и запятой.

Все предикатные и функциональные символы имеют определенное число аргументов. Если их число равно N, говорят, что мы имеем дело с N-местный (или N-арным) предикатным (функциональным) символом.
Термом называется или переменная или константа или функциональный символ, аргументы которого являются термами. Терм, не содержащий переменных, называется константным или основным.

Формула в логике предикатов – это или предикат, аргументы которого являются термами(в этом случае формула называется атомной или элементарной), или последовательность, получаемая одним из следующих способов из некоторых формул А и Б и некоторой переменной x:
1) НЕ А
2) А И Б
3) А ИЛИ Б
4) А->Б (т.е.из А следует Б)
5) СУЩ x А (т.е. существует x такое, что справедливо А)
6) ВСЕ x А (т.е. при всех x справедливо А).

В формулах 5) и 6) А называется областью действия соответствующего квантора.
При этом если x из этих формул входит в область действия, то такая переменная называется связанной, а в противном случае – свободной.
Положительным литералом называется атомная формула, отрицательным литералом – отрицание атомной формулы.
Конъюнктивной нормальной формой формулы называется конъюнкция конечного числа дизъюнктов. Предваренной (префиксной) нормальной формой называется представление формулы в виде:
КВАНТОР1 x1, …, КВАНТОРN xN А
Здесь КВАНТОР1,…,КВАНТОРN – это один из кванторов СУЩ или ВСЕ, а все это выражение называется префиксом, формула А не содержит кванторов и называется матрицей.
Сколемовской нормальной формой называется предваренная нормальная форма, не содержащая кванторов существования.

На практике для обработки знаний представленных в виде логики предикатов используется метод резолюции хорновских дизъюнктов.
Дизъюнкт – это дизъюнкция (соединение при помощи ИЛИ) конечного числа литералов. Хорновскими называют дизъюнкты, содержащие не более одного положительного литерала.

Дата добавления: 2015-07-15