HOL

HOL rövid magasabb rendű Logic egy programozási környezet, amelyben tételek bizonyítja és bizonyítási eszközök végrehajtani.
Beépített döntéshozatali eljárással és a tétel Provers automatikusan létrehozza sok egyszerű tételek. Az Oracle mechanizmust biztosít hozzáférést a külső programok, mint a műholdas és a BDD motorok.
HOL 4 különösen alkalmas, mint a platform végrehajtására kombinációi levonása, a végrehajtás és a tulajdon ellenőrzése.

Mi az új ebben a kiadásban:

• HolSmtLib már támogatja Z3 bizonyítéka Újjáépítési célokat érintő fix szélességű szavak és a fordítás HOL be SMT-lib 2 formátumban.
• HolQbfLib támogatja ellenőrzése mind érvényességét, és a tanúsítvány érvénytelenségének megállapítása a Squolem 2.02. wordsSyntax.mk_word_replicate kiszámítja a szélessége a kapott szót alkalmazni egy szám és egy fix-szélességű szó.
• A rendszer támogatja szintaxis decimális törtek.
• Ez a szintaxis térképek divízió szempontjából formájában n / 10m.
• A központi rendszer, ez a forma engedélyezve van a valódi, racionális, és összetett elméletek.

Mi az új a 6-os verzió:

• A HolSmtLib könyvtár már támogatja bizonyítéka Újjáépítési SMT megoldó Z3 .
• Sok típusú változókat most elemzett és nyomtatásra kisbetűs görög betűkkel.
• határolt átírja jobban működnek.
• egyszerűsítése szempontjából járó EL üzemeltető jobb.
• Továbbfejlesztett támogatás bag műveletek.
• Syntax frissítések a dolgok, mint az egyetemes set.
• Egyéb kisebb javítások és a hibajavítás.