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

Как я его понял, он предлагает не столько доказательство того, что модель описывает систему, которая достигнет определенного результата, сколько доказательство правильности самой модели (что модель, например, не начнет в какой-то момент делить на ноль где-то внутри себя, или не зациклится в самый неожиданный момент). Я имел в виду и то, и другое, просто часто одни свойства можно вывести из других (простым способом). Т.е. вообще говоря, нет нужды приводить доказательства всех свойств, нужны доказательства некоторых ключевых. Тут надо пояснить, что отладка (логических) моделей отличается от отладки программ. С моделями основная проблема - что они могут оказаться невыполнимы. С точки зрения логики, это значит что из них можно вывести False, а из False - что угодно. Таким образом, теряется смысл формального обоснования. Т.е. первое требование при импорте модели, чтобы она была выполнима. В онтологиях типа OWL этот вопрос специально решался использованием дескрипционных логик, для которых есть практичные алгоритмы разрешимости. И которые позволяют отвечать на некоторые другие вопросы (типа классификации, проверки принадлежности индивидуала модели и т.д.). А в более сложном случае, дескрипционных логик не хватает. При этом этот более сложный случай не за горами, ибо после онтологий, все уже хотят использовать rules совместно с онтологиями :).