Понятие формальной системы. Основой логических моделей является понятие формальной системы, задаваемой четверкой M = (T, P, A, F).

Основой логических моделей является понятие формальной системы, задаваемой четверкой M = (T, P, A, F).

Множество T есть множество базовых элементов различной природы, например слов из некоторого ограниченного словаря. Предполагается, что существует процедура П(Т) проверки принадлежности произвольного элемента множеству Т.

Множество P есть множество синтаксических правил. С их помощью из элементов T образуют синтаксически правильные выражения, например, из слов ограниченного словаря строятся синтаксически правильные выражения. Должна существовать процедура П(Р), позволяющая определить, является ли

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

В множестве Р выделяется подмножество А априорно истинных выражений (аксиом). Должна существовать процедура П(А) проверки принадлежности любого синтаксически правильного выражения множеству А.

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

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

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

Использование логик различного типа при построении синтаксических и семантических правил порождает логические модели различных типов.

Математический аппарат, применяемый в логических моделях знаний

Логические модели представления знаний строятся на основе двух видов исчислений – исчисления высказываний и исчисления предикатов первого порядка.