axiom-solver

This content is not available in your language yet.

Компилирует поддерживаемый арифметико-логический фрагмент Axiom в SMT-LIB2. В отличие от v0.1, постусловия действительно транслируются, а не оставляются как TODO. Production-backend должен вызывать Z3/cvc5 и валидировать либо реконструировать solver evidence.

Связанные исследования

Этот компонент входит в исследовательский проект Axiom. Все компоненты собраны по теме localzet-axiom. Основной язык документации — русский. Исследовательские результаты и ограничения не означают готовность к промышленному применению.

Исходный код · MIT