OSDN -- Open-Source-Software-Entwicklung und Downloads
Übersetzungsstatus von Deutsch translation status for de

RSS
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.

2012-07-28 13:51
7

HolSmtLib unterstützt nun auch die Z3 Beweis Wiederaufbau für Ziele, bei denen festgelegtem Wörter und eine Übersetzung von HOL in SMT-LIB-2-Format. HolQbfLib unterstützt die Überprüfung für Gültigkeit und Ungültigkeit von Zertifikaten für 2.02 Squolem. wordsSyntax.mk_word_replicate berechnet die Breite des resultierenden Wortes bei Anwendung auf eine Ziffer und ein Wort mit fester Breite. Das System unterstützt die Syntax für Dezimalbrüche. Diese Syntax ordnet Teilung Begriffen der Form n / 10 m. In das Kernsystem ist diese Syntax für die realen, rationalen und komplexen Theorien aktiviert.
Tags: Enhancements, Bugfixes, Stable
HolSmtLib now also supports Z3 proof reconstruction for goals that involve fixed-width words and a translation from HOL into SMT-LIB 2 format. HolQbfLib supports checking for both validity and invalidity of certificates for Squolem 2.02. wordsSyntax.mk_word_replicate computes the width of the resulting word when applied to a numeral and a fixed-width word. The system supports syntax for decimal fractions. This syntax maps to division terms of the form n / 10m. In the core system, this syntax is enabled for the real, rational, and complex theories.

2011-01-04 10:29
6

Die Bibliothek unterstützt jetzt HolSmtLib Beweis Wiederaufbau für die SMT-Solver Z3. Viele Typ-Variablen können nun analysiert und ausgedruckt werden als Kleinbuchstaben griechischen Buchstaben. Bounded schreibt besser funktionieren. Vereinfachung der Bedingungen, die die EL Betreiber ist besser. Verbesserte Unterstützung für Beutel Operationen. Syntax-Updates für Dinge wie die Grundgesamtheit. Weitere kleine Verbesserungen und Bugfixes.
The HolSmtLib library now supports proof reconstruction for the SMT solver Z3. Many type variables can now be parsed and printed as lower-case Greek letters. Bounded rewrites work better. Simplification of terms involving the EL operator is better. Improved support for bag operations. Syntax updates for things like the universal set. Other minor enhancements and bugfixes.

2009-07-17 20:22
5

Es gibt jetzt eine Poly / ML Umsetzung der HOL4 für Benutzer auf anderen Plattformen als Windows. Eine Überlastung kann jetzt target "syntaktischen Mustern". Die: String-Typ ist nun ein Alias für: char Liste. Typen können nun Ziffern. Die Finite-kartesisches Produkt "Array"-Typ kann jetzt mit eckigen Klammern geschrieben werden. wordsLib unterstützt jetzt Auswertung über Nicht-Standard-Wort-Größen. Unterstützung für Unicode wurde hinzugefügt. Unterstützung für Patricia Bäume wurde hinzugefügt. Viele andere Verbesserungen und Bugfixes wurden.
Tags: Enhancements, Bugfixes, Poly/ML, Unicode
There is now a Poly/ML implementation of HOL4 available for users on platforms other than Windows. Overloading can now target "syntactic patterns". The :string type is now an alias for :char list. Types can now be numerals. The finite cartesian product "array" type can now be written with square brackets. wordsLib now supports evaluation over non-standard word-sizes. Support for Unicode was added. Support for Patricia trees was added. Many other enhancements and bugfixes were made.

2007-01-14 12:00
4

New set Verständnis Notation wurde hinzugefügt. SML-String-Notation wurde hinzugefügt. Unterstützung für den XEmacs-Editor wurde hinzugefügt. Case-Ausdrücke können nun auch Literale als Muster. Induktive Definitionen werden nun im Hinblick auf eine unterschiedliche Monoset gemacht. Typen, die abgekürzt Muster verwenden in abgekürzter Form gedruckt. Support für rationale Zahlen und fester Länge Zahlen wurde hinzugefügt. Fehler verhinderte, dass einige Komponenten im Rahmen der Erstellung von GCC 4 festgelegt worden sind. Normalisierung in natürlichen Zahlen und Zahlen festgesetzt worden war. Handhabung von leeren Saiten wurde behoben.
Tags: Major feature enhancements
New set comprehension notation was added. SML
string notation was added. Support for the XEmacs
editor was added. Case expressions may now include
literals as patterns. Inductive definitions are
now made with respect to a varying monoset. Types
that use abbreviated patterns are printed in
abbreviated form. Support for rational numbers and
fixed-length integers was added. Bugs that
prevented some components from compiling under GCC
4 were fixed. Normalization in natural numbers and
integers was fixed. Handling of empty strings was
fixed.

2006-01-30 05:15
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

Project Page Download: Bugtracker Download: Änderungsprotokoll Download: CVS Homepage Download: Liste Download: TGZ