HOL

HOL krótkie Wyższej Zamów Logic jest środowisko programistyczne, w których można udowodnić twierdzenia i narzędzia dowód realizowane.
Wbudowane procedury decyzyjne i dowodzenie twierdzenie może automatycznie nawiązać wiele prostych twierdzeń. Mechanizm Oracle daje dostęp do zewnętrznych programów takich jak silniki SAT i BDD.
HOL 4 jest szczególnie przydatny jako platforma dla kombinacji odliczenia, realizacji i kontroli własności realizacji

Co nowego w tym wydaniu:.

• HolSmtLib obsługuje również Z3 dowód przebudowę na cele, które obejmują stałe szerokości słowa i tłumaczenie ze Hol w formacie SMT-LIB 2.
• HolQbfLib obsługuje sprawdzanie ważności i nieważności zarówno certyfikatów dla Squolem 2,02. wordsSyntax.mk_word_replicate oblicza szerokości wynikowego słowo po nałożeniu na cyfrze i stałej szerokości słowa.
• System obsługuje składnię ułamki dziesiętne.
• W tej składni mapy do warunków podziału postaci n / 10m.
• W systemie głównym, składnia ta jest włączona dla rzeczywistych, racjonalnych i skomplikowanych teorii.

Co nowego w wersji 6:

• Biblioteka HolSmtLib obsługuje dowód rekonstrukcji dla solver SMT Z3 .
• Wiele zmiennych typu można obecnie analizowany i drukowane małymi literami alfabetu greckiego.
• ograniczone przepisuje działać lepiej.
• Uproszczenie terminów związanych z operatorem EL jest lepiej.
• Ulepszone wsparcie dla operacji workowych.
• aktualizacje składni dla rzeczy jak uniwersalny zestaw.
• Inne drobne ulepszenia i poprawki.