Наложение онтологических соглашений и ограничений целостности и их проверка

В документе описывается технология формирования и проверки онтологических соглашений и ограничений целостности, налагаемых на информационные единицы, формируемые по некоторой метаинформации. Дата последней модификации документа: 08 сентября 2022.

Введение

Механизмы задания и проверки непротиворечивости баз знаний и данных (то есть онтологических соглашений и ограничений целостности), сформированных в виде иерархических сетей, формируемых на основе 2-уровневой модели порождения информации, являются расширением механизмов проверки полноты информационных ресурсов. Их необходимость обоснована тем фактом, что применяемая модель формирования информационных ресурсов не может в полной мере охватить все ограничения предметной области, накладываемые на задаваемую информацию.

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

Формирование условий

Ограничения целостности формируются в виде предикатов (логических формул) на основе специального языка и в терминах некоторой модели онтологии, то есть с использованием вершин некоторого (одного) инфоресурса типа "метаинформация" (Задание ограничений целостности между терминами разных баз знаний, то есть составленных по разными онтологиям, в настоящее время не поддерживается). Язык описания таких формул задан в информационном ресурсе "Язык описания контекстных условий" (типа "метаинформация"), который расположен в общем Фонде (раздел "Платформа IACPaaS", папка "Ядро платформы"). Структура языка заимствуется из области знаний «Математика» с некоторыми упрощениями (присутствует не весь перечень логических, арифметических, теоретико-множественных и т.п. операций) и дополнениями (для осуществления навигации по информационным ресурсам и работы с их содержимым). Сформированные контекстные условия (то есть содержащий их информационный ресурс, сформированный по указанной метаинформации) сопоставляются инфоресурсу типа "метаинформация", в терминах которого записаны данные условия, после чего все сформированные на его основе базы знаний (ресурсы типа "информация") могут быть проверены на соответствие этим условиям. (Это означает, что сформированы они могут быть и в форме, нарушающей условия, однако, информация о несоответствиях доступна пользователю.)

Для формирования ограничений целостности, зарегистрированный пользователь должен:

получить из общего Фонда ссылку на инфоресурс "Язык описания контекстных условий" (выполняется один раз)
в личном фонде создать новый инфоресурс типа "информация", используя полученный в доступ "Язык описания контекстных условий" в качестве метаинформации
открыть созданный инфоресурс на редактирование (используется базовый или JS редактор) и наполнить его контекстными условиями, соблюдая полноту

Любое контекстное условие на верхнем уровне начинается с одного из трёх кванторов:

квантор всеобщности (для любого Х выполняется Y)
квантор существования (существует Х, для которого выполняется Y)
квантор существования и единственности (существует единственный Х, для которого выполняется Y)

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

Переменная (X) задаётся в виде пары "имя" - "область возможных значений" (ОВЗ), где ОВЗ задаётся как подграф "имени" одним из следующих способов (соответствующих заданию терма-множества):

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

Типы логической формулы (Y):

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

Ниже приведено упрощённое представления языка описания контекстных условий (в нотации текстового представления информационных ресурсов):

Язык описания контекстных условий
{
  ~set ~new контекстное условие {
    ~proxy кванторные формулы ~ALT{
      ~new квантор всеобщности {
        ~proxy переменная и формула {
          ~one ~new -> Язык описания запросов$/.../переменная;
          ~new формула ~ALT{
            ~new равенство {
              ~new левая часть {
                ~new -> Язык описания запросов$/.../терм;
              }
              ~new правая часть {
                ~new -> Язык описания запросов$/.../терм;
            }}
            ~new неравенство {
              ~proxy -> равенство;
            }
            ~proxy арифметические отношения ~ALT{
              ~new больше или равно {
                ~proxy два числа {
                  ~new левое число {
                    ~new -> Язык описания запросов$/.../терм-число;
                  }
                  ~new правое число {
                    ~new -> Язык описания запросов$/.../терм-число;
              }}}
              ~new больше {
                ~proxy -> два числа;
              }
              ~new меньше или равно {
                ~proxy -> два числа;
              }
              ~new меньше {
                ~proxy -> два числа;
            }}
            ~proxy теоретико-множественные отношения ~ALT{
              ~new принадлежность элемента множеству {
                ~proxy терм и множество {
                  ~new -> левая часть;
                  ~new правая часть {
                    ~new -> Язык описания запросов$/.../терм-множество;
              }}}
              ~new непринадлежность элемента множеству {
                ~proxy -> терм и множество;
              }
              ~new множество есть собственное подмножество другого множества  {
                ~proxy множество и множество {
                  ~new левая часть {
                    ~new -> Язык описания запросов$/.../терм-множество;
                  }
                  ~new -> правая часть;
              }}
              ~new множество есть несобственное подмножество другого множества  {
                ~proxy -> множество и множество;
              }
              ~new множество не есть подмножество другого множества {
                ~proxy -> множество и множество;
            }}
            ~proxy формулы с пропозициональными связками ~ALT{
              ~new импликация {
                ~new условие {
                  ~new -> формула;
                }
                ~new заключение {
                  ~new -> формула;
              }}
              ~new равносильность {
                ~new левая часть {
                  ~new -> формула;
                }
                ~new правая часть {
                  ~new -> формула;
              }}
              ~new конъюнкция {
                ~seq конъюнкт {
                  ~new -> формула;
              }}
              ~new дизъюнкция {
                ~seq дизъюнкт {
                  ~new -> формула;
              }}
              ~new исключающее или {
                ~seq -> дизъюнкт;
              }
              ~new отрицание {
                ~new -> формула;
              }
              ~new  ["истина"] 
              ~new  ["ложь"] 
            }
            ~proxy -> кванторные формулы;
            ~new прямой предок {
              ~new предок {
                ~new -> Язык описания запросов$/.../терм;
              }
              ~new потомок {
                ~new -> Язык описания запросов$/.../терм;
            }}
            ~new равенство подграфов {
              ~proxy -> равенство;
            }
            ~new соответствие регулярному выражению {
              ~new строка {
                ~new -> Язык описания запросов$/.../терм-строка;
              }
              ~new регулярное выражение [str]
      }}}}
      ~new квантор существования {
        ~proxy -> переменная и формула;
      }
      ~new квантор существования и единственности {
        ~proxy -> переменная и формула;

}}}}

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

переменная (указывается ссылка на переменную, определенную ранее, т.е. "выше" в графе контекстного условия)
термы, связанные с множествами (не присутствует явно, делится на: множество соответствующих мета-пути вершин - см. далее, экстенсиональное задание множества - см. выше, действия над множествами - включает некоторые операции из описания переменной Х выше, а также операции: мощность множества - число элементов, Supremum - наибольший элемент, Infimum - наименьший элемент)
арифметические термы (не присутствует явно, делится на: сумма, произведение, разность, частное, возведение в степень, абсолютная величина)
кванторные конструкции (не присутствует явно, детали - ниже)
условный терм (см. выше)
метка вершины (возвращается имя или значение вершины)
константы (не присутствует явно, делится на: пустое множество, целочисленная константа, вещественная константа, логическая константа, строковая константа, темпоральная константа - дата и время, двоичная константа - бинарные данные, текущий момент)
именованная математическая постоянная (не присутствует явно, делится на: π, τ, e - вещественные числа)
взять оригинал (возвращается вершина, являющаяся оригиналом указанной)
конкатенация (применима только к строкам)
соответствующая мета-пути вершина (подробнее - см. ниже)

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

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

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

Задание выполняется следующим образом:

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

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

Формальное описание "переменной" и "термов" различных типов даётся в документе "Конструирование и выполнение запросов к базам знаний и данных".

Более подробно об используемых конструкциях можно узнать в статье Т.Л. Гаврилова, А.С. Клещев, Внутренняя модель математической практики для систем автоматизированного конструирования доказательств теорем. Ч.2. Модель математического диалекта, Пробл. управл., 2006, выпуск 5, 68–73.

Когда инфоресурс с контекстными условиями наполнен и полон, его необходимо подключить к метаинформации, для которой он был составлен. Для этого необходимо открыть на редактирование инфоресурс метаинформации, перейти в меню "контекст", нажать кнопку-иконку (+f) для задания инфоресурса контекстных условий, после чего выбрать этот ресурс в фонде пользователя, нажав соответствующую ему кнопку-иконку (+f), отображаемую только у инфоресурсов подходящего типа (созданных по метаинформации "Язык описания контекстных условий").

Рис.1. Подключение ИР с контекстными условиями к ИР онтологии

После этого также можно отключить инфоресурс с контекстными условиями от онтологии (воспользовавшись кнопкой-иконкой Корзина) и подключить иной инфоресурс с контекстными условиями (отключив имеющийся с помощью кнопки-иконки Корзина, а затем подключив иной инфоресурс так же, как указано выше).

Проверка условий

Проверка КУ возможна только, если содержащий их информационный ресурс полон. Механизм, отвечающий за проверку имеющихся контекстных условий применительно к конкретной базе, доступен в двух режимах (в обоих из них в начале работы выполняется проверка полноты КУ):

через API доступа к инфоресурсам
как составная часть базового редактора Платформы

Работа механизма состоит в проверке всех КУ путём последовательного перебора. Если значение логической формулы какого-то условия есть ложь, контекстное условие считается не выполненным. При этом проверка оставшихся КУ прекращается и формируется текстовое сообщение о том, на каких данных (фрагмент подграфа базы наблюдений) и какая формула дала значение ложь.

API

Проверка контекстных условий не является составной частью тех методов API, которые отвечают за создание вершин (их структурирование в графе базы знаний и назначение им меток), так как выполнение данных проверок при каждом создании вершины или её удалении или изменении метки может существенно замедлить процесс модификации графа базы знаний. Поэтому данный механизм доступен через вызов метода checkContextFormulas() у объекток типа инфоресурс (Inforesource). Результат работы метода - пустая строка, если все КУ выполнены, или некоторый текст о нарушении некоторого КУ (см. выше). Также при возникновении ошибки во время проверки КУ будет создано исключение типа StorageException, с указанием подробностей ошибки в его тексте.

Важно отметить, что инфоресурс, для которого необходимо выполнить проверку КУ, должен быть подключён в решатель (в качестве собственного) или сервис (в качестве входного или выходного), чтобы быть доступным для чтения при выполнении БП. Инфоресурс его онтологии или инфоресурс КУ подключать не требуется и не требуется иметь к ним доступ.

Применение этого механизма целесообразно в агентах, которым для работы необходимо удоствериться в том, что выполнены все КУ для обрабатываемых информационных ресурсов.

Редактор

Процесс проверки КУ выполняется в рамках меню "контексте" и состоит в:

отправке пользователем команды на запуск проверки КУ (по нажатию кнопки запуска проверки в соответствующем подпункте меню "инфо" редактора - кнопка доступна, если к онтологии обрабатываемого ИР прикреплён ИР с контекстными условиями, для которого выполнена полнота)
выполнении редактором проверки КУ (так как это может быть длительный процесс, то в этот момент пользователь в интерфейсе редактора видит сообщение о том, что проверка ведётся уже определённое время, и кнопку обновления состояния)
отображении результата проверки (в момент, когда пользователь, обновит состояние редактора, а результат проверки уже получен)

Схема проверки КУ в редакторе приведена ниже:

Рис.2. Выполнение проверки контекстных условий в редакторе базы знаний (пример - далее).

Пример

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

имена всех признаков попарно различны
нижняя граница значений признака не превышает верхнюю границу

При совместном редактировании баз вполне возможно нарушение первого условия - когда разные пользователи вносят один и тот же признак в разные группы на основе своих представлений. Второе условие может нарушаться по неосторожности (перепутывание границ при вводе).

Ниже представлена модель онтологии базы наблюдений:

Онтология наблюдений
{
  ~setmm ~new группа признаков
  {
    ~setmm ~new -> группа признаков;
    ~setmm ~new признак
    {
      ~one ~new нижняя граница [real]
      ~one ~new верхняя граница [real]
    }
  }
}

Для описания контекстных условий формируется отдельный целевой инфоресурс (по метаинформации "Язык описания контекстных условий").

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

указание на необходимость выполнить перебор всех пар из 2 признаков (то есть перебор пар вершин, сформированных по метапонятию "признак")
установление факта того, что они различны (то есть это две разные вершины базы наблюдений)
подтверждение того факта, что их имена (то есть метки этих вершин) различны

Такое условие задаётся так:

КУ баз наблюдений <<< Платформа IACPaaS/Ядро платформы/Язык описания контекстных условий
{
  контекстное условие [имена признаков попарно различны] {
    квантор всеобщности {
      переменная [признак1] {
        терм-множество {
          множество соответствующих мета-пути вершин {
            начало пути {
              вершина {
                инфоресурс [-> Онтология наблюдений$/группа признаков/признак;]
      }}}}}
      формула {
        квантор всеобщности {
          переменная [признак2] {
            терм-множество {
              область возможных значений переменной {
                переменная [-> признак1;]
          }}}
          формула {
            импликация {
              условие {
                формула {
                  неравенство {
                    левая часть {
                      терм {
                        переменная [-> признак1;]
                    }}
                    правая часть {
                      терм
                      {
                        переменная [-> КУ баз наблюдений$/имена признаков попарно различны/квантор всеобщности/формула/квантор всеобщности/признак2;]
              }}}}}
              заключение {
                формула {
                  неравенство {
                    левая часть {
                      терм {
                        метка вершины {
                          терм {
                            переменная [-> признак1;]
                    }}}}
                    правая часть {
                      терм {
                        метка вершины {
                          терм {
                            переменная [-> признак2;]
}}}}}}}}}}}}}}

Особенности составления данного КУ следующие:

два признака задаются через два квантора всеобщности: для любого "признак1" и для любого "признак2"
ОВЗ "признак2" берётся как ОВЗ "признак1" - это поможет сократить расчёты, так как такое ОВЗ вычисляется 1 раз (для первого признака), а в противном случае число вычислений ОВЗ равнялось бы числу признаков + 1 (1 раз вычисляется для "признак1" и затем по количеству признаков несколько раз вычисляется для "признак2", что не требуется, так как эти множества не меняются)
использована "импликация" - ЕСЛИ разные признаки, ТО разные имена

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

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

Такое условие задаётся так:

КУ баз наблюдений <<< Платформа IACPaaS/Ядро платформы/Язык описания контекстных условий
{
  контекстное условие [нижняя граница больше верхней] {
    квантор всеобщности {
      переменная [признак] {
        терм-множество {
          множество соответствующих мета-пути вершин {
            начало пути {
              вершина {
                инфоресурс [-> Онтология наблюдений$/группа признаков/признак;]
      }}}}}
      формула {
        меньше {
          левое число {
            терм-число {
              метка вершины {
                терм {
                  соответствующая мета-пути вершина {
                    начало пути {
                      переменная [-> КУ баз наблюдений$/нижняя граница больше верхней/квантор всеобщности/признак;]
                    }
                    продолжение пути {
                      элемент пути [1] {
                        инфоресурс [ -> Онтология наблюдений$/группа признаков/признак/нижняя граница;]
          }}}}}}}
          правое число {
            терм-число {
              метка вершины {
                терм {
                  соответствующая мета-пути вершина {
                    начало пути {
                      переменная [-> КУ баз наблюдений$/нижняя граница больше верхней/квантор всеобщности/признак;]
                    }
                    продолжение пути {
                      элемент пути [1] {
                        инфоресурс [ -> Онтология наблюдений$/группа признаков/признак/верхняя граница;]
}}}}}}}}}}}}

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