Уровни работы с ISO 15926 презентация

ISO 15926:7 - First Order Logic
ActualIndididual(x) → PossibleIndividual(x)
«Темплейты» ISO 15926:7 (FOL/rewriting)
ApprovalTriple(x, y, z) ↔ Approval(x) & hasApproved(x, y) & hasApprover(x, z)
OIM (Object Information Model)
Domain specific templates???
DSL — internal/external (e.g. Python)

oriented
определены поверх аксиоматики на языке First Order Logic (Prover9)
аксиомы/темплейты нормативны в 15926:7, т.е. де-факто reference implementation
Альтеранативный вариант — ISO 15926:8 реализация поверх OWL
Широкий набор OWL инструментария

ActualIndividual одновременно является ClassOfIndividual
«Референсная» проверка — относительно аксиоматики 15926:7
«Разворачиваем» темплейты
Проверяем, что полученный набор утверждений выполним относительно аксиоматики

lots of others)
Трансляция в DL logics
Provers: FaCT++, Pellet, RacerPro, HermiT
Трансляция в SAT (propositional logics)
Не уверен, что всегда возможна прямая трансляци, но можно использовать incremental подход
Другие логики HOL/Type-theory
Избыточно, но удобно для встраивания в языки и для мета-теор. целей

примеру, тормозит на абстрактных класс
из-за недетерминизма (OR-branching)
Большие размеры моделей
O(a*n)/O(b*n2) для унарных/бинарных предикатов
Все описание обрабатывается одновременно
возможно разбиение на подзадачи

те же структуры данных
Создание инструментария и DSL
Быстрая проверка на ошибки критична для юзабилити
Сообщения об ошибках
К примеру, Осман уже реализовал :)
Мега-мета-проект: 15926L :)

(отношения) задаем список инстансов (пар), которые ему принадлежат
Проверяем (конечную) модель на соответствие аксиомам
Медленно, нужны оптимизации
сотни предикатов/1000+ аксиом
бинарные отношения - O(n2)
недетерминизм
Надо учитывать особенности аксиоматики

∃ (плюс предикаты и константы)
Берем все константы — исходное множество инстансов
F преобразуем дизъюнктивную форму вида (A&B&C)|(D&E&F)|..|(X&Y&Z)
Or-branching — экспонента в worst-case
Перебираем конъюнкты A(a)&B(b)&C(d)
Исходное множество утверждений
Выводим новые, используя аксиомы
Если модель непротиворечива - win
Все конъюнкты противоречивы - fail

добавляем C(a)
A(x)&..&B(x) → C(x)|D(x)
Or-branching
Дважды-экспоненциально в worst-case!
~(A(x)&..B(x))
Эквивалентно A(x)&..&B(x) → False
Если аксиома применима — противоречие
A(x)&..&B(x) → ∃u Φ(u,x)
Добавляем новые инстансы в модель
Потенциально неограниченные модели!
В 15926:2 к счастью ограниченны :)

моделей
намекается в стандарте :)
Похоже можно избавится от бинарных отношений (e.g. hasClassifier(x,y))
Резко сокращает размеры моделей
«Линейные» (компактные) модели
В стандарте не намекается, но скорее всего :)
Недетерминизм в основном вызван трансляцией abstract class, но не только

примерно и было — EXPRESS language
Удобнее для встраивания в DSL
Проблемы с использованием сущ. языков
Множественное наследование
Oneof (далеко не во всех языках)
Недетерминизм
Abstract class трансляция

алгоритма
Инкрементальный (проверяем по частям)
Компактные модели
оптимизации недетерминизма
оптимизации AND-branhing, быстрые проверки конфликтов
Хранилище данных
Можно сделать эффективнее чем triple-store