HOL

HOL kort van Hoër Orde Logika is 'n programmeertaal omgewing waarin stellings bewys kan word en bewys gereedskap geïmplementeer.
Ingeboude besluit prosedures en stelling provers kan outomaties vestig baie eenvoudige stellings. 'N binneste vertrek meganisme gee toegang tot eksterne programme soos SAT en BDD enjins.
HOL 4 is veral geskik as 'n platform vir die implementering van kombinasies van aftrekking, uitvoering en eiendom nagaan

Wat is nuut in hierdie release:.

• HolSmtLib ondersteun nou ook Z3 bewys rekonstruksie vir doelwitte wat behels vaste wydte woorde en 'n vertaling van HOL in SBS-LIB 2 formaat.
• HolQbfLib ondersteun nagaan vir beide geldigheid en ongeldigheid van sertifikate vir Squolem 2.02. wordsSyntax.mk_word_replicate bere die wydte van die gevolglike woord wanneer dit toegepas word om 'n syfer en 'n vaste-wydte woord.
• Die stelsel ondersteun sintaksis vir desimale breuke.
• Dit sintaksis kaarte afdeling terme van die vorm N / 10m.
• In die kern stelsel, is hierdie sintaksis in staat gestel om vir die ware, rasionele en komplekse teorieë.

Wat is nuut in die weergawe 6:

• Die HolSmtLib biblioteek ondersteun nou bewys rekonstruksie vir die SBS oplosser Z3 .
• Baie tipe veranderlikes kan nou ontleed word en gedruk as laer-geval Griekse letters.
• Begrens herskryf werk beter.
• Vereenvoudiging van terme wat die EL operateur is beter.
• Verbeterde ondersteuning vir sak bedrywighede.
• Syntax updates vir dinge soos die universele stel.
• Ander klein verbeterings en bugfixes.