2.2.Онтология базы знаний проектируемой интеллектуальной системы

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

Абсолютные понятия:

• Тождественно истинная формула

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

Синонимы: Тавтология Пример: А или ¬А принимает значение “1”

• Тождественно ложная формула

Определение: Формула является тождественно ложной, если она принимает значение "ложь" ("0") при любых входящих в нее значениях переменных.

Пример: А и ¬А принимает значение “0”

• Модус Ponens

Определение: если A и A→B — выводимые формулы, то B также выводима.

Синонимы: правило заключений.

• Модус Darii Определение: Если всякий термин M есть термин P иесли всякий термин S есть термин M, то всякий термин S есть термин P.

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

• Метатеория Определение: это множество свойств всевозможных формальных теорий. Синонимы: metatheory.

• Логическая функция

Определение: Логическая функция - это функция принимающая значение 0 или 1.

Пример: тождественная функция

Синонимы: logic function,множество логических функций.

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

Относительные понятие:

• Непротиворечивость Определение: свойство формальной теории, заключающееся в невыводимости из неё противоречия. Синонимы: сonsistency

• Каноническая система Определение: Каноническая система определяется собственным алфавитом констант А , алфавитом переменных X конечным множеством аксиом и конечным множеством правил вывода. Синонимы: canonical system.

• Ассоциативное исчисление или система Туэ Определение:Система подстановок или полусистема Туэ – это формальная система, определяемая алфавитом A и правилом вывода Rj.

• Система подстановок или полусистема Туэ Определение: Система подстановок или полусистема Туэ - это формальная система, определяемая алфавитом A и правилом вывода Ri.

Утверждения:

• Теорема Геделя(Первая) Пояснение: Любая формальная теория T, содержащая формальную арифметику, неполна : в ней существует(и может быть эффективно построена) замкнутая формула F, такая что отрицание F истинно , но ни F, ни отрицание F не выводимы в T.

• Теорема Геделя (Вторая) Пояснение: для любой непротиворечивой формальной теории T, содержащей формальную арифметику, формула, выражающая непротиворечивость T, недоказуема в T.

• Теормема Поста о нормальной форме Пояснение: Для любой канонической системы CS с алфавитом A существует нормальная каноническая система NS над A, эквивалентная CS (т.е множество теорем NS над A и множество теорем CS совпадают).