Исследователи представили методологию встраивания модальной логики первого порядка (FML) в классическую логику высшего порядка (HOL) с использованием системы Isabelle/HOL. Работа расширяет подходы глубокого и поверхностного встраивания, предлагая три различных метода реализации семантики Крипке с постоянной областью, что критически важно для формальной верификации сложных интеллектуальных систем и автоматизированного доказательства теорем в ИИ.
Данное исследование решает проблему представления модальных операторов, таких как необходимость и возможность, в рамках стандартных инструментов автоматического доказательства. Авторы сравнивают три подхода: глубокое встраивание, «тяжеловесное» максимальное поверхностное и «легковесное» минимальное поверхностное встраивание. Каждый из методов предлагает разный баланс между выразительностью логики и вычислительной эффективностью при проверке формальных спецификаций.
Разработка позволяет более эффективно использовать инструменты автоматического вывода для анализа агентных систем, где требуется моделирование знаний, убеждений или временных состояний. Предложенные методы упрощают интеграцию модальных рассуждений в существующие пайплайны формальной верификации, обеспечивая высокую точность доказательств при работе с кванторами и модальностями в рамках одной среды.
Ключевые факты
- Исследование реализовано в среде интерактивного доказательства теорем Isabelle/HOL.
- Представлены три типа встраивания: глубокое, максимальное поверхностное и минимальное поверхностное.
- Работа сфокусирована на модальной логике первого порядка (FML) с семантикой Крипке с постоянной областью.
- Методология направлена на повышение автоматизации при проверке сложных логических моделей в ИИ.
- Результаты опубликованы в виде расширенного препринта на платформе arXiv.