Downloadliste

Projektbeschreibung

Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking.

Systemanforderungen

Die Systemvoraussetzungen sind nicht definiert
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.

2006-01-30 05:15 Zurück zur Release-Liste
3

Diese Veröffentlichung fügt Theorien über Ko-induktive (evtl. unendlich) gekennzeichnet Übergang Wege in pathTheory, und für die Sortierung und Liste Permutationen sortingTheory. Es wird ein neuer erster Ordnung Beweis Taktik (METIS_TAC genannt), die eine geordnete Auflösung und Paramodulation verwendet, und eine "boolification" Werkzeug, das automatisch definiert Funktionen, die Zuordnung von Datentypen boolean Vektoren. Viele Erweiterungen, Bugfixes, und rückwärts kompatibel sind.
Tags: Major feature enhancements
This release adds theories of co-inductive (possibly infinite) labelled transition paths in pathTheory, and of sorting and list permutations in sortingTheory. It adds a new first-order proof tactic (called METIS_TAC) that uses an ordered resolution and paramodulation, and a 'boolification' tool that automatically defines functions that map data types to boolean vectors. Many extensions, bugfixes, and backwards incompatibilities.

Project Resources