Логические основы интеллектуальных систем

Методы логического вывода являются одними из основных компонентов интеллектуальных систем пополнения знаний.

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

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

Реализация логического представления знаний возможна в логических системах дедуктивного (с фиксированным механизмом вывода) и индуктивного (с механизмом вывода, конструируемом на основании обучающих примеров) типов.

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

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

Модус поненс (modus ponens) «если истина формула А, и истинно, что из А следует В, то истинна и формула В».

Модус толлендо толленс (modus tollendo tollens) «если из А, следует В и В ложно, то и А ложно».

Правило резолюции, основанное на тавтологии

⊩ (А∨С, В∨ не С) ⟶ А∨В.

Пусть Е – это множество формул, тогда запись Е ⊨ А означает, что если все формулы из Е истинны, то будет истинной формула А. В этом случае А называется логическим следствием из Е.

Принцип дедукции состоит в следующем. Формула А является логическим следствием конечного множества Е тогда и только тогда, когда ЕÈ{неА} содержит невыполнимые формулы.

Заметим, что не всегда алгоритм дедукции оказывается более эффективным по сравнению с подходом, основанным на алгебраическом представлении вывода (использующем эквивалентные преобразования из А в В).

Резолюция – это прием, используемый при дедуктивном выводе, заключающийся в нахождении двух дизъюнктов А∨С, В∨ не С, один из которых содержит литеру, а другой - ее отрицание. На основании этого сравнения формируется новый дизъюнкт, называемый резольвентой. Порождение новых дизъюнктов является основой метода резолюций, широко применяемого в интеллектуальных системах.

Принцип резолюции

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

Главная идея принципа резолюции, как правила вывода, заключается в проверке того, содержит ли множество дизъюнктов R пустой (ложный) дизъюнкт. Обычно резолюция применяется с прямым или обратным методом рассуждения.

Прямой метод из посылок А, А®В выводит заключение В (правило modus ponens). Недостаток прямого метода состоит в его не направленности: повторное применение метода приводит к резкому росту промежуточных заключений, не связанных с целевым заключением.

Обратный вывод является направленным: из желаемого заключения В и тех же посылок он выводит новое подцелевое заключение А. Каждый шаг вывода в этом случае связан всегда с первоначально поставленной целью.

Процесс доказательства методом резолюции (от обратного) состоит из следующих этапов:

1. Предложения или аксиомы приводятся к дизъюнктивной нормальной форме;

2. К набору аксиом добавляется отрицание доказываемого утверждения в дизъюнктивной форме;

3. Выполняется совместное разрешение этих дизъюнктов, в результате чего получаются новые, основанные на них дизъюнктивные выражения (резольвенты);

4. Генерируется пустое выражение, означающее противоречие;

5. Подстановки, использованные для получения пустого выражения, свидетельствуют о том, что отрицание отрицания истинно.

Существенный недостаток метода Резолюции заключается в формировании на каждом шаге вывода множества резольвент – новых дизъюнктов, большинство из которых является лишними.