Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction. Now available: Isabelle2008 Some notable improvements: * HOL: significant speedup of Metis prover; proper support for multithreading. * HOL: new version of primrec command supporting type-inference and local theory targets. * HOL: improved support for termination proofs of recursive function definitions. * New local theory targets for class instantiation and overloading. * Support for named dynamic lists of theorems.
This site is an experimental HTML rendering of fragments of the IsarMathLib project. IsarMathLib is a library of mathematical proofs formally verified by the Isabelle theorem proving environment. The formalization is based on the Zermelo-Fraenkel set theory. The Introduction provides more information about IsarMathLib. The software for exporting Isabelle's Isar language to HTML markup is at an early beta stage, so some proofs may be rendered incorrectly. In case of doubts, compare with the Isabelle generated IsarMathLib proof document.
In the fully expansive (or LCF-style) approach to theorem proving, theorems are represented by an abstract type whose primitive operations are the axioms and inference rules of a logic. Theorem proving tools are implemented by composing together the inference rules using ML programs. This idea can be generalised to computing valid judgements that represent other kinds of information. In particular, consider judgements (a,r,t,b), where a is a set of boolean terms (assumptions) that are assumed true, r represents a variable order, t is a boolean term all of whose free variables are boolean and b is a BDD. Such a judgement is valid if under the assumptions a, the BDD representing t with respect to r is b, and we will write a r t --> b when this is the case. The derivation of "theorems" like a r t --> b can be viewed as "proof" in the style of LCF by defining an abstract type term_bdd that models judgements a r t --> b analogously to the way the type thm models theorems |- t.
HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: 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 (users may have to prove the hard theorems themselves!) 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. several widely used versions of the HOL system: 1. HOL88 from Cambridge; 2. HOL90 from Calgary and Bell Labs; 3. HOL98 from Cambridge, Glasgow and Utah. HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL.
HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.
* Higher-Order Logic * o HOL (Higher-Order Logic) o HOLCF (Higher-Order Logic of Computable Functions) * First-Order Logic * o FOL (Many-sorted First-Order Logic) o ZF (Set Theory) o CCL (Classical Computational Logic) o LCF (Logic of Computable Functions) o FOLP (FOL with Proof Terms) * Miscellaneous * o Sequents (first-order, modal and linear logics) o CTT (Constructive Type Theory) o Cube (The Lambda Cube)
Vampire is winning at least one division of the world cup in theorem proving CASC since 1999. All together Vampire won 17 titles: more than any other prover. We traditionally take part in the following two divisions of the competition: * The FOF division: unrestricted first-order problems. This division was ranked second in importance after the MIX division before 2007 and is now recognised as the main competition division. * The CNF division: first-order problems in conjunctive normal form. This division was called MIX before 2007 and recognised as the main competition division. We also participate in other, more special competition divisions but Vampire is not specialised for them so our achievements are mostly modest.
This is a home page for logical frameworks providing pointers to further material, including a bibliography, implementations, some researchers in the area, and recent announcements and papers. logical framework is a formal meta-language for deductive systems. The primary tasks supported in logical frameworks to varying degrees are * specification of deductive systems, * search for derivations within deductive systems, * meta-programming of algorithms pertaining to deductive systems, * proving meta-theorems about deductive systems. I include here systems that in other places have been called meta-logics and meta-logical frameworks; for me the choice of terminology merely indicates the relative emphasis placed on these tasks. Logical frameworks have been applied to many examples from logic and the theory of programming languages.