# Différences

Cette page vous donne les différences entre la révision choisie et la version actuelle de la page.

proof_assistants [Le 30/01/2019 à 18:13] jaxom depl astuces |
— (Version actuelle) | ||
---|---|---|---|

Ligne 1: | Ligne 1: | ||

- | ===== Proof assistants ===== | ||

- | \\ | ||

- | Proof assistants are computer programs that aids a human to prove things (so they are sometimes called /theorem provers/). Generally, they understand several formal logics with there rules and are able to apply those rules, automatically or guided by the human verifier. Such tools are at the core of the verification process.\\ | ||

- | |||

- | \\ | ||

- | ==== Coq ==== | ||

- | \\ | ||

- | Coq is a proof assistant environment.\\ | ||

- | |||

- | * License: GNU LGPL 2.1\\ | ||

- | * Web site: http://coq.inria.fr/\\ | ||

- | * Debian packages: coq coq-doc proofgeneral-coq\\ | ||

- | |||

- | \\ | ||

- | ==== ACL2 ==== | ||

- | \\ | ||

- | ACL2 is an environment where programs are described using an applicative subset of Common Lisp. Each function of the program entered in the environment is formally proven (termination, ...).\\ | ||

- | |||

- | * License: GNU GPL\\ | ||

- | * Web site: http://www.cs.utexas.edu/users/moore/acl2/\\ | ||

- | * Debian packages: acl2 acl2-books acl2-books-certs\\ | ||

- | acl2-books-source acl2-doc acl2-emacs acl2-infix acl2-infix-source\\ | ||

- | acl2-source\\ | ||

- | |||

- | ==== Milawa ==== | ||

- | \\ | ||

- | Milawa is a "self-verifying" theorem prover for an ACL2-like logic.\\ | ||

- | |||

- | We begin with a simple proof checker, call it A, which is short enough to verify by the "social process" of mathematics.\\ | ||

- | |||

- | We then develop a series of increasingly powerful proof checkers, call them B, C, D, and so on. We show that each of these is sound: they accept only the same formulas as A. We use A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is sound, we can trust B, and so on for C, D, and the rest.\\ | ||

- | |||

- | Our final proof checker is really a theorem prover; it can carry out a goal-directed proof search using assumptions, calculation, rewrite rules, and so on. We use this theorem prover to discover the proofs of soundness for B, C, and so on, and to emit these proofs in a format that A can check. Hence, "self verifying."\\ | ||

- | |||

- | * License : GNU GPL 2+\\ | ||

- | * Web site: http://userweb.cs.utexas.edu/users/jared/milawa/Web/\\ | ||

- | |||

- | ==== Phox ==== | ||

- | \\ | ||

- | %%PhoX%%is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version.\\ | ||

- | |||

- | * License: [[ce_cill-b|CeCILL-B]]\\ | ||

- | * Web site:\\ | ||

- | http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/phox.html\\ | ||

- | |||

- | \\ | ||

- | |||

- | ==== HOL Light ==== | ||

- | \\ | ||

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

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://www.cl.cam.ac.uk/users/jrh/hol-light/\\ | ||

- | |||

- | ==== HOL Zero ==== | ||

- | \\ | ||

- | HOL Zero is a new, basic theorem prover for the HOL logic, designed with trustworthiness as its top priority. It is primarily intended for two roles:\\ | ||

- | |||

- | * highly-trustworthy system for checking and/or consolidating proofs created on other theorem provers;\\ | ||

- | * pedagogical example of a simple theorem prover and its implementation.\\ | ||

- | |||

- | Note that some proof porting mechanism is required for the role of checking/consolidating proofs. One such mechanism is under development at Proof Technologies.\\ | ||

- | |||

- | Unlike other HOL systems, HOL Zero is NOT primarily targetted at developing proofs, although it is suitable for simple natural deduction proofs. It concentrates on doing basic functionality well, and has relatively sophisticated term parsing, pretty printing and error reporting. Its source code is very carefully written and commented, and aims to be as simple and readable as possible. An extensive glossary of HOL-related terminology is provided as part of the user documentation.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://www.proof-technologies.com/holzero.html\\ | ||

- | |||

- | ==== Holfoot ==== | ||

- | \\ | ||

- | Holfoot is an implementation of Smallfoot inside the HOL 4 theorem prover. In addition to the features supported by Smallfoot it can handle data and supports interactive proofs. Moreover, it can handle arrays. It is described in detail in my dissertation.\\ | ||

- | |||

- | Simple specifications with data like copying a list can be handled automatically. More complicated ones like fully functional specifications of filtering a list, mergesort, quicksort or an implementation of red-black trees require user interaction. During this interaction all the features of the HOL 4 theorem prover can be used, including the interface to external SMT solvers like Yices.\\ | ||

- | |||

- | HOL 4 is needed to run Holfoot interactively. For purely automated useage precompiled command-line versions are available.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://holfoot.heap-of-problems.org/\\ | ||

- | |||

- | ==== HOL ==== | ||

- | \\ | ||

- | HOL 4 is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. [[built_-in|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.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://hol.sourceforge.net/\\ | ||

- | |||

- | ==== PVS ==== | ||

- | \\ | ||

- | PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.\\ | ||

- | |||

- | * License: GNU GPL\\ | ||

- | * Web site: http://pvs.csl.sri.com/\\ | ||

- | |||

- | ==== Isabelle ==== | ||

- | \\ | ||

- | 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. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.\\ | ||

- | |||

- | Compared with similar tools, Isabelle's distinguishing feature is its flexibility. Most proof assistants are built around a single formal calculus, typically higher-order logic. Isabelle has the capacity to accept a variety of formal calculi. The distributed version supports higher-order logic but also axiomatic set theory and several other formalisms. See logics for more details.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://isabelle.in.tum.de/ | ||

- | |||

- | ==== Dedukti ==== | ||

- | |||

- | Dedukti is a universal proof checker, based on the λΠ-calculus modulo. | ||

- | The project is named after the word for "to deduce" in Esperanto. | ||

- | |||

- | * License: Cecill-B | ||

- | * Web site: http://dedukti.gforge.inria.fr/ | ||

- | |||

- | ==== ProofPower ==== | ||

- | |||

- | ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. The suite comprises the following packages: | ||

- | |||

- | * PPDev - The ProofPower developer kit, mainly comprising SLRP, a parser generator for Standard ML. | ||

- | * PPTex - The ProofPower interface to TeX and LaTeX. | ||

- | * PPXpp - The X Windows/Motif front-end for ProofPower. | ||

- | * PPHol - The HOL specification and proof development system. | ||

- | * PPZed - The Z specification and proof development system. | ||

- | * PPDaz - The Compliance Tool for specifying and verifying Ada programs. | ||

- | |||

- | All the ProofPower packages except PPDaz are free, open-source, software. | ||

- | |||

- | * License: GNU GPL | ||

- | * Web site: http://www.lemma-one.com/ProofPower/index/ | ||

- | |||

- | ==== HOL4 ==== | ||

- | |||

- | The HOL interactive theorem prover is a 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 SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: https://hol-theorem-prover.org | ||

- | |||

- | ==== Lean ==== | ||

- | |||

- | Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. | ||

- | |||

- | The Lean project was launched by Leonardo de Moura at Microsoft Research in 2013. It is a collaborative open source project, hosted on GitHub. Contributions to the code base and library are welcome. | ||

- | |||

- | You can experiment with an online version of Lean that runs in your browser, or use an online tutorial. | ||

- | |||

- | * License: Apache 2.0 | ||

- | * Web site: https://leanprover.github.io/ | ||

- | |||

- | |||