Средства эффективной диагностики ошибок для систем логического прототипирования

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