HOL

HOL короткое Высшую Заказать логика программирования среда, в которой теоремы может быть доказано и доказательство инструменты реализованы.
Встроенные процедуры принятия и доказательства теорем может автоматически установить много простых теорем. Механизм Oracle предоставляет доступ к внешним программам, таким как двигатели САТ и BDD.
HOL 4 особенно подходит в качестве платформы для реализации комбинации вычет, исполнения и контроля имущества

Что нового В этом выпуске:.

• HolSmtLib теперь также поддерживает Z3 доказательства реконструкции для целей, которые включают равноширинные слова и перевод с HOL в формате SMT-LIB 2.
• HolQbfLib поддерживает проверку для обоих действия и недействительности сертификатов для Squolem 2.02. wordsSyntax.mk_word_replicate вычисляет ширину получаемого слова применительно к цифрой и фиксированной ширины слова.
• Система поддерживает синтаксис для десятичных дробей.
• Это синтаксис карты в Отдел точки зрения формы н / 10м.
• В базовой системы, этот синтаксис включен для реальных, рациональных и комплексных теорий.

Что нового в версии 6:

• Библиотека HolSmtLib теперь поддерживает доказательства реконструкции для SMT решателя Z3 .
• Многие переменные типа в настоящее время может быть разобран и печатается как строчные греческие буквы.
• Ограниченные переписывает работать лучше.
• Упрощение условий, связанных с оператором EL лучше.
• Улучшена поддержка мешок операций.
• Обновления синтаксис вещи, как универсального множества.
• Другие незначительные улучшения и исправления.