HOL

HOL court à partir d'ordre supérieur Logic est un environnement de programmation dans lequel théorèmes peuvent être prouvées et les outils de preuve mis en œuvre.
Procédures de décision intégrés et démonstrateurs peuvent automatiquement établir plusieurs théorèmes simples. Un mécanisme d'Oracle donne accès à des programmes externes tels que les moteurs SAT et BDD.
HOL 4 est particulièrement approprié comme une plate-forme pour la mise en œuvre des combinaisons de déduction, l'exécution et le contrôle des biens

Ce qui est nouveau dans cette version:.

• HolSmtLib prend également en charge la reconstruction Z3 preuve objectifs qui impliquent des mots à largeur fixe et une traduction de HOL au format SMT-LIB 2.
• HolQbfLib prend en charge le contrôle à la fois la validité et l'invalidité des certificats pour Squolem 2,02. wordsSyntax.mk_word_replicate calcule la largeur du mot résultant lorsqu'elle est appliquée à un chiffre et une largeur fixe mot.
• Le système supporte la syntaxe pour les fractions décimales.
• Cette syntaxe cartes à des peines de division de la forme n / 10m.
• Dans le système de base, cette syntaxe est activée pour les théories réelles, rationnels, et complexes.

Quoi de neuf dans la version 6:

• La bibliothèque prend désormais en charge la reconstruction HolSmtLib preuve de la SMT solveur Z3 .
• Beaucoup de variables de type peuvent maintenant être analysées et imprimées en lettres minuscules grecques.
• réécritures bornées fonctionnent mieux.
• Simplification des termes impliquant l'opérateur EL est mieux.
• Amélioration du support pour les opérations de sac.
• Mises à jour de syntaxe pour des choses comme l'ensemble universel.
• D'autres améliorations et corrections mineures.