Формальные логические модели представления знаний.

Формальные логические модели – это модели, основанные на формальных исчислениях, в качестве таких исчислений используются различные математ.-логические модели-языки, которые позволяют делать логический вывод на основе имеющихся правил и аксиом.

В логических моделях знания представляются в виде совокупности правильно построенных формул какой-либо формальной системы, которая задается четверкой (T,P,A,R):

Т – множество базовых элементов;

Р – множество синтаксических правил;

А – множество аксиом ФС, которые в рамках данной ФС априорно считаются истинными;

R – конечное множество правил вывода.

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

В основе ФЛМ лежит понятие высказывание – это атомарное предложение на этом формальном языке.

В качестве таких моделей могут использоваться:

· пропозициональная логика (простые высказывания +|&→↔)

· логика 1ого порядка (добавляются кванторы общности и существования, предикаты, логические функции)

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

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

Получение знаний может быть разделено на два вида:

· в БЗ сообщается новое высказывание, и алгоритм вывода выводит все возможные заключения для этого высказывания.

· при сообщении высказывания в БЗ ей нужно доказать истинность/ложность этого утверждения.

Был разработан наиб. эфф. алгоритм вывода – метод резолюций.

Преимущества данной модели:

· краткость, БЗ может быть записана в нескольких универсальных законах

· вычислительная эффективность

· несложность конструирования

· мощные правила вывода

Недостатки данной модел и:

· представление знаний в таких моделях не наглядно.

· не эффективно обозначить свойства и отношения однотипными логическими функциями.

· описание знаний в виде лог. формул не позволяет проявится преим. которые имеют автоматические системы обработки структур данных.

Этапы создания БЗ ФЛМ:

1. Идентификация задания. Определение того, что должна решать ваша БЗ (доказательство, вывод).

2. Определение релевантных знаний.

3. Определение словаря предикатов функций и конструкций, на этом этапе происходит преобразование релевантных данных предметной области в формальные понятия. Результатом этого этапа является – онтология предметной области. Она определяет какие объекты существуют, но не определяют их конкретную взаимосвязь и свойства.

4. регистрация общих знаний о предметной области:

· определение аксиом

· написание атомарных выражений

· полное высказывание по БЗ

5. Передача (организация) запросов к процедуре логического вывода и получение ответов.

6. отладка БЗ

· проверка алгоритма вывода

· наличие тестового набора запросов

· проверка аксиом (ее истинность/ложность может быть проверена независимо от основной БЗ)

· проверка конкретных выражений

 

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

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

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

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

p q s n p q s n (если то)

Каждое хорновское выражение может быть записано как импликация, предпосылкой которой является конъюнкция положительных литералов, а заключением— один положительный литерал.

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

Хорновское выражение без положительных литералов может быть записано как импликация, заключением которой является литерал False.

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

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

Алгоритм прямого логического вывода начинает работу с известных фактов в БЗ. Если известны все предпосылки некоторой импликации (выражения), то ее заключение добавляется к множеству известных фактов. Этот процесс продолжается до тех пор, пока запрос не выводится как факт, либо дальнейший вывод становится невозможным. Можно легко убедиться в том, что алгоритм прямого логического вывода является непротиворечивым: каждый этап логического вывода по сути представляет собой применение правила отделения. Кроме того, алгоритм прямого логического вывода является полным: в нем может быть получено каждое атомарное высказывание, которое следует из базы знаний.

Алгоритм обратного логического вывода действует в обратном направлении от запроса. Если удается сразу же узнать, что выск., содержащееся в запросе q, является истинным, то не нужно выполнять никакой работы. В противном случае алгоритм находит те импликации в базе знаний, из которых следует g. Если можно доказать, что все предпосылки одной из этих импликаций являются истинными, то высказывание g также является истинным.

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