- •Предисловие
- •Глава1. Логика классическая
- •1.1. Логика высказываний
- •1.1.1. Алгебра высказываний
- •1.1.1.2. Правила записи сложных формул
- •1.1.1.3. Законы алгебры высказываний
- •1.1.1.4. Эквивалентные преобразования формул
- •1.1.1.5. Нормальные формы формул
- •1.1.2. Исчисление высказываний
- •1.1.2.1. Интерпретация формул
- •1.1.2.2. Аксиомы исчисления высказываний
- •1.1.2.3. Метод дедуктивного вывода
- •1.1.2.4. Метод резолюции
- •Вопросы и задачи
- •Расчетно-графическая работа
- •1. 2. Логика предикатов
- •1.2.1. Алгебра предикатов
- •1.2.1.1. Логические операции
- •1.2.1.2. Правила записи сложных формул
- •1.2.1.3. Законы алгебры предикатов
- •1.2.1.4. Эквивалентные преобразования формул
- •1.2.1.2. Предварённая нормальная форма
- •1.2.1.3. Сколемовская стандартная форма
- •1.2.2. Исчисление предикатов
- •1.2.2.1. Интерпретация формул
- •1.2.2.2. Аксиомы исчисления предикатов
- •1.2.2.3. Правила унификации предикатов
- •1.2.2.4. Метод дедуктивного вывода
- •1.2.2.5. Метод резолюции
- •1.2.3. Логическое программирование
- •1.2.3.1. Основы логического программирования*
- •1.2.3.2. Подготовка среды Visual Prolog для работы
- •1.2.3.3. Описание логических задач на языке Prolog
- •Вопросы и задачи
- •Расчетно-графическая работа
- •Формула
- •1.3. Логика реляционная
- •1.3.1. Реляционная алгебра*
- •1.3.1.1. Унарные операции
- •1.3.1.2. Бинарные операции
- •1.3.2. Реляционное исчисление*
- •1.3.3. Языки реляционной логики
- •Вопросы и задачи
- •Расчетно-графическая работа
- •Глава 2. Неклассическая логика
- •2.1. Нечёткая логика
- •2.1.1. Нечёткие множества
- •2.1.2. Нечёткая алгебра
- •2.1.2.1. Операции над нечёткими множествами
- •2.1.2.2. Законы нечёткой алгебры
- •2.1.2.3. Свойства нечётких отношений
- •4.4.2. Экспертные системы
- •Вопросы и задачи
- •Расчетно-графическая работа
- •2.2. Модальная логика
- •2.2.1. Темпоральная (или временнáя) логика*.
- •Ответы и решения
- •Литература
- •Предметный указатель
1. 2. Логика предикатов |
99 |
• принять x = f(w) и удалить x:
F= w y((P1 (a) P2 (f(w)) P3.(y))&(¬P2 (w) P2 (f(w)) P3.(y))& (¬P2(w)
¬P1(a) P3.(y))).
Множество дизъюнктов матрицы К={(P1 (a) P2
(f(w)) P3.(y)),
(¬P2(w) P2(f(w)) P3.(y)), (¬P2(w)¬P1(a) P3.(y))}.
Обратите внимание, что в одном из дизъюнктов есть контрарные атомы, но один из них содержит предметную переменную w, а другой – сколемовскую функцию f(w). Это - ¬P2 (w) и P2 (f(w). В двух других дизъюнктах также есть контрарные атомы, но содержащие предметную постоянную ‘а’. Это - P1 (a) и ¬P1 (a). При исполнении алгоритма по принципу резолюции выполняется поиск и унификация таких атомов.
1.2.2. Исчисление предикатов
Если выполнить подстановку вместо пропозициональных переменных исчисления высказываний формулы алгебры предикатов, то каждая схема доказательства теоремы и каждая схема вывода заключения сохраняются в исчислении предикатов. Однако для кванторных операций следует дать интерпретацию формул логики предикатов и выделить правила и аксиомы, позволяющие управлять кванторами и выполнять унификацию предикатов.
1.2.2.1. Интерпретация формул
Под интерпретацией формул следует понимать систему, состоящую из непустого множества V, называемого
универсумом, и отображения предиката P( t1,t2,…, tn) на
100 |
Математическая логика |
двухэлементное множество {и, л}. Предметные постоянные ti и функциональные символы fi(t1, t2,..., ) есть элементы t V, а предметные переменные есть обычные переменные, заданные на универсуме. Символы логических и кванторных операций приобретают также обычный смысл. Тогда каждому предикату P(t1,t2,…, tn), принявшему значение «и» или «л», ставится в соответствие n-местное отношение на множестве V.
Например, если V - множество целых чисел и дано частное суждение x y z(P(x, f+(y, z))):= «существует число x, которое меньше суммы чисел y и z», то при х=5, у=1, z=3 имеем двухместную операцию f+(1, 3) и двухместное отношение между числом 5 и значением операции f+(1,3)=4. Отображение P(5,4) на двухэлементное множество дает значение «л». Это же суждение при х=5, у=2, z=4
имеет f+(2,4)=6 и P(5, 6)=«и» (см. рис. 1.10.)
Другими словами, интерпретация функциональных символов определяется по значениям функции на универсуме, а интерпретация предикатных символов по отображению на множество {и, л}.
1. 2. Логика предикатов |
101 |
Выделяют три класса формул: тождественно истинные, тождественно ложные и выводимые.
Тождественно истинные формулы - это особый класс формул, которые при исполнении логических и кванторных операций принимают значение «истины» для всех интерпретаций предметных постоянных, функциональных и предикатных символов. Большинство из них - аксиомы исчисления предикатов.
Например, формула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)=и, то не для всех х F(x)=и».
102 |
Математическая логика |
Вывод заключения из множества посылок есть:
F1,F2,…, Fn| B,
где слева от знака “| ” записывают множество посылок и необходимых аксиом F1,F2,…, Fn, а справа – заключение B. На естественном языке эта запись читается так: «верно, что В выводимо из посылок и аксиом F1,F2,…, Fn».
Другая форма вывода заключения:
F1,F2 ,...,Fn
B,
где над чертой - множество посылок и аксиом F1,F2,…, Fn, а под чертой - заключение B.
Вывод заключения на языке математической логики это доказательство теоремы | F1&F2&…&Fn→B. В процессе доказательства последовательно используют аксиомы и законы логики предикатов, правила введения и удаления кванторов, правила подстановки и унификации предикатов. При выводе используют правила modus ponens и modus tollens.
1.2.2.2. Аксиомы исчисления предикатов
Аксиомы исчисления предикатов опираются на двенадцать аксиом исчисления высказываний, сохраняя при этом особенности исполнения кванторных операций. Поэтому для понимания механизма вывода в исчислении предикатов следует знать правила введения и удаления кванторов. Эти правила существенно облегчают преобразования сложных логических формул.
П1.Удаление квантора всеобщности: если выводима формула x(F(x)), то, заменив предметную переменную x на терм t, можно удалить квантор всеобщности и получить выводимую формулу
1. 2. Логика предикатов |
103 |
x (F(x)) F(t).
П2. Введение квантора всеобщности:
a)если выводима формула F(t), то, заменив терм t на предметную переменную x, можно ввести квантор всеобщности и получить выводимую формулу
F(t)
xF(x).
b) если выводима формула (F1(t)→F2(x)) и F1(t) не содержит свободной переменной x, то выводима формула
F1(t) → F2 (x) .
F1(t) → x (F2 (x))
П3. Удаление квантора существования: если выводима формула x(F(x)), то, заменив предметную переменную х на предметную постоянную ‘а’, можно удалить квантор существования и получить выводимую формулу
x (F(x) F(a).
П4. Введение квантора существования:
a) если выводима формула F(t), то, заменив терм t на предметную переменную x в заданной области интерпретации, можно ввести квантор существования и получить выводимую формулу
F(t)xF(x).
b) если выводима формула F1(x)→F2(t) и F2 не содержит свободной переменной x, то выводима формула
F1(x) → F2 (t) .x (F1(x)) → F2 (t)
П5. Формирование ПНФ формулы:
a) если при исполнении логических операций один из предикатов Fi не содержит переменной x, связанной в