Без заголовка

Тут всё не просто. Единственная реально проработанная формальная аксиоматика в ISO 15926 - это аксиоматика Части 2 выполненная на FOL в Части 7 для работы с аксиомами темплейтов. Соответственно эта часть может быть формально верифицирована, но это не OWL, это ризонеры типа Prover 9, и проблема в том, что аксиоматикой темплейтов занимаются не многие, и стандарта для представления аксиом нет. А то что называется представлением ISO 15926 в OWL - это всего лишь формат сериализации, RDF с использованием ряда предикатов OWL. Самый простой пример - это специализации и классификации. Они не выражены в виде subClassOf и type, они встречаются в виде реифицированных отношений части 2 или инстансов темплейтов. Так что никакой OWL ризонер их не возьмёт. Более сложные примеры - это классы классов, тут предлагается использовать punning, и я что-то не уверен, что есть хоть один ризонер, умеющий учитывать punning и делать на этой основе выводы. Этот комплекс проблем собирается решить рабочая группа по Части 12 стандарта, её ещё называют группой по OWL 2 представлению. Однако что они собираются делать с необходимой для функционирования стандарта реификацией практически всех отношений - мне пока не ясно. Поэтому мы являемся сторонниками специализированных верификаторов и потихоньку развиваем их на базе нашего Editor. Собственно отчёт об итогах хакатона Онтолог Саммита включён в отчёты о наших прочих попытках верификации: http://15926.org/viewtopic.php?f=5&t=154