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 краще.
• Покращена підтримка мішок операцій.
• Оновлення синтаксис для таких речей, як універсальної множини.
• Інші незначні поліпшення і виправлення.