ИСТИНА

Isabelle/HOL обеспечивает довольно продвинутую и надежную поддержку для достижения целей доказательства с помощью внешних решателей SMT путем реконструкции результирующего дерева доказательств в ядре логического вывода Isabelle/Pure. В частности, в настоящее время Isabelle полностью и эффективно поддерживает восстановление доказательств для бескванторных фрагментов теорий равенства и неинтерпретируемых функций (QF_UF) и линейной целочисленной арифметики (QF_LIA). Тем не менее, существует ряд практически значимых теорий, решение которых можно решить с помощью относительно эффективных алгоритмов, но они не поддерживаются ни процедурой восстановления доказательства Isabelle, ни самими решателями SMT. Между тем, если решающая процедура для расширенной логической теории может быть выражена как полная стратегия инстанцирования бескванторных формул, которая сокращает данную проблему решения до поддерживаемого логического фрагмента (QF_UFLIA), теория может быть полностью поддержана в рамках существующей инфраструктуры Isabelle/HOL с относительно небольшими дополнительными усилиями. Целью нашей работы было разработать полностью формальное доказательство полноты для эффективной стратегии инстанцирования бескванторных формул, которая переводит проблему выполнимости из логики ограниченной линейной целочисленной арифметики (называем ее QF_BLIA) в равносильную задачу в логике линейных целых чисел, арифметические и неинтерпретируемые функции (QF_UFLIA). Полученные формальные доказательства строго следуют представленному неформальному изложению доклада, но в то же время они также содержат довольно значительное количество вспомогательных идей, которые потенциально могут быть обобщены для других подобных формализаций доказательств и автоматизированы с использованием Isabelle/ML.