HOL

HOL кратко от по-висш порядък Logic е програмна среда, в която теореми може да бъде доказано и инструменти се отварят изпълнени.
Вградени процедури решения и теорема доказващите може автоматично да създават много прости теореми. Механизъм Наложеното дава достъп до външни програми като SAT и БДД двигатели.
HOL 4 е особено подходящ като платформа за прилагане на комбинации на приспадане, изпълнение и контрол имот

Какво ново в тази версия:.

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

Какво ново във версия 6:

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