Уровни работы с ISO 15926 «Ассемблер» ISO 15926:2 - EXPRESS actual_individual, class_of_class Аксиомы 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)

Нажмите для полного просмотра!

Содержание ▲

Вы можете ознакомиться и скачать презентацию на тему Уровни работы с ISO 15926 «Ассемблер» ISO 15926:2 - EXPRESS actual_individual, class_of_class Аксиомы 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). Доклад-сообщение содержит 12 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1

Описание слайда:

Уровни работы с ISO 15926 «Ассемблер» ISO 15926:2 - EXPRESS actual_individual, class_of_class Аксиомы 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)

Слайд 2

Описание слайда:

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

Слайд 3

Описание слайда:

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

Слайд 4

Описание слайда:

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

Слайд 5

Описание слайда:

Зачем делать свою реализацию? Производительность/масштабируемость FOL слишком мощная для 15926:7: гибко, но медленно К примеру, тормозит на абстрактных класс из-за недетерминизма (OR-branching) Большие размеры моделей O(a*n)/O(b*n2) для унарных/бинарных предикатов Все описание обрабатывается одновременно возможно разбиение на подзадачи

Слайд 6

Описание слайда:

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

Слайд 7

Описание слайда:

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

Слайд 8

Описание слайда:

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

Слайд 9

Описание слайда:

Построение модели (аксиомы) A(x)&..&B(x) → C(x) Если все A(a)..B(a) есть в текущей модели, добавляем 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 к счастью ограниченны :)

Слайд 10

Описание слайда:

Особенности аксиоматики 15926:2 Единственный источник конфликтов disjoint аксиомы (one_of(Class1, Class2 etc)) Достаточно конечных моделей намекается в стандарте :) Похоже можно избавится от бинарных отношений (e.g. hasClassifier(x,y)) Резко сокращает размеры моделей «Линейные» (компактные) модели В стандарте не намекается, но скорее всего :) Недетерминизм в основном вызван трансляцией abstract class, но не только

Слайд 11

Описание слайда:

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

Слайд 12

Описание слайда:

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

Теги Уровни работы 15926 Ассемблер EXPRESS actual individual class Аксиомы First

Похожие презентации