# Différences

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

automatic_theorem_provers [Le 16/08/2017 à 21:49] david_mentre Ajout Princess |
— (Version actuelle) | ||
---|---|---|---|

Ligne 1: | Ligne 1: | ||

- | ====== Automatic theorem provers ====== | ||

- | |||

- | ==== Zenon ==== | ||

- | |||

- | Zenon is an automatic theorem prover that handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: http://focal.inria.fr/zenon/ | ||

- | |||

- | ==== MetiTarski ==== | ||

- | |||

- | MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving //real-valued special functions// such as log, exp, sin, cos and sqrt. In particular, it is designed to prove //universally quantified inequalities// involving such functions. This problem is undecidable, so MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful. | ||

- | |||

- | * License: MIT | ||

- | * Web site: http://www.cl.cam.ac.uk/~lp15/papers/Arith/ | ||

- | |||

- | ==== E Theorem Prover ==== | ||

- | |||

- | E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms. | ||

- | |||

- | If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it’s of the form “there exists an X with property P”), the latest versions can also provide possible answers (values for X). | ||

- | |||

- | * License: GNU GPL | ||

- | * Web site: http://www4.informatik.tu-muenchen.de/~schulz/E/E.html | ||

- | |||

- | |||

- | ==== SPASS ==== | ||

- | |||

- | SPASS is an automated theorem prover for first-order logic with equality. | ||

- | |||

- | * License: BSD | ||

- | * Web site: http://www.spass-prover.org/ | ||

- | |||

- | ==== Spike ==== | ||

- | |||

- | SPIKE is an automated theorem prover using (first-order) formula-based Noetherian induction. Spike can be called from the Coq proof assistant using a tactic that automatically performs lazy and mutual induction. We provide a zip file with the Coq scripts using this tactic. Spike proofs can be checked with Coq. | ||

- | |||

- | * License: BSD | ||

- | * Web site: https://code.google.com/p/spike-prover/ | ||

- | |||

- | ==== Psyche ==== | ||

- | |||

- | Psyche is a modular platform for automated or interactive theorem proving, programmed in OCaml and built on an architecture (similar to LCF) where a small kernel interacts with plugins and decision procedures: | ||

- | |||

- | * The kernel is based on a proof-search engine à la Prolog, offering an API to perform incremental and goal-directed constructions of proof-trees in (a standard but carefully chosen) Sequent Calculus, which can be seen as a tableau method. | ||

- | * Psyche can produce proof objects. | ||

- | * Plugins can be programmed to drive the kernel, using its API, through the search space towards an answer provable or not provable; soundness of the answer only relies on the kernel via the use of a private type for answers (similar to LCF’s theorem type). | ||

- | * Plugins can be interactive. | ||

- | * Psyche offers a memoisation feature to help programming efficient plugins. | ||

- | * The kernel is parameterised by a procedure deciding the consistency of collections of literals with respect to a background theory, just as in SAT-modulo-theories (SMT) solvers. | ||

- | |||

- | |||

- | * License: CeCILL-C | ||

- | * Web site: http://www.lix.polytechnique.fr/~lengrand/Psyche/ | ||

- | |||

- | ==== PolyPaver ==== | ||

- | |||

- | A numerical theorem prover with support for verifying floating-point programs in SPARK/Ada. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: https://michalkonecny.github.io/polypaver/_site/index.html | ||

- | |||

- | ==== Stallax ==== | ||

- | |||

- | Satallax is an automated theorem prover for higher-order logic. The particular form of higher-order logic supported by Satallax is Church's simple type theory with extensionality and choice operators. The SAT solver MiniSat is responsible for much of the search for a proof. Satallax generates propositional clauses corresponding to rules of a complete tableau calculus and calls MiniSat periodically to test satisfiability of these clauses. | ||

- | |||

- | * License: BSD like | ||

- | * Web site: https://mathgate.info/satallax/ | ||

- | |||

- | ==== Zipperposition ==== | ||

- | |||

- | Zipperposition is intended to be a superposition prover for full first order logic, plus some extensions (datatypes, recursive functions, arithmetic). The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces or graphviz files for nice graphical display. | ||

- | |||

- | Zipperposition supports several input formats: | ||

- | * TPTP (fof, cnf, tff) | ||

- | * TIP | ||

- | * its own native input, extension .zf | ||

- | |||

- | |||

- | * License: BSD like | ||

- | * Web site: https://github.com/c-cube/zipperposition | ||

- | |||

- | ==== Leo-III ==== | ||

- | |||

- | The automated theorem proving systems LEO-I and LEO-II have found international acclaim as very successful reasoners for classical higher-order logic. Novel contributions of LEO-I include a native (versus axiomatic) treatment of the extensionality principles and the cooperation with external reasoners (such as the first-order prover E) via a flexible agent architecture. The implementation of LEO-II did significantly influence the parallel development of the new higher-order TPTP THF infrastructure for typed higher-order logics, which in turn has led to major system improvements (e.g. in the automated theorem provers ISABELLE/HOL and TPS) and to new systems developments (such as Satallax) for classical higher-order logic. LEO-II has won the international CASC competitions in 2010 and it has been integrated in the interactive proof assistant ISABELLE /HOL. | ||

- | |||

- | In this project, we want to turn LEO-II into a state-of-the-art theorem prover based on ordered paramodulation/ superposition. In constrast to LEO-II, we replace the internal term representation (the commonly used simply typed lambda calculus) by a more expressive system supporting type polymorphism. In the course of the project, we plan to further enhance the type system with type classes and type constructors similar to System Fω . In order to achieve a substantial performance speed-up, the architecture of Leo-III will be based on massive parallelism (e.g. And/Or-Parallelism, Multisearch). | ||

- | |||

- | The current design is a multi-agent blackboard architecture that will allow to independently run agents with our proof calculus as well as agents for external (specialized) provers. Leo-III will focus right from the start on compatibility to the widely used TPTP infrastructure. Moreover, it will offer built-in support for specialized external prover agents and provide external interfaces to interactive provers such as Isabelle/HOL. The implementation will excessively use term sharing and several indexing techniques. Leo-III will also offer special support for reasoning in various quantified non-classical logics by exploiting a semantic embedding approach. | ||

- | |||

- | |||

- | * License: BSD like | ||

- | * Web site: http://page.mi.fu-berlin.de/lex/leo3/ | ||

- | |||

- | |||

- | ==== Princess ==== | ||

- | |||

- | Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala. Princess can reason about problems in integer arithmetic, augmented with predicates that can be axiomatised arbitrarily. Such problems can contain arbitrary quantifiers to express that some formula is supposed to hold for all or for some integers. | ||

- | |||

- | Main features of Princess include: | ||

- | |||

- | * Decision + quantifier elimination procedure for Presburger arithmetic. | ||

- | * Modules for various theories beyond Presburger: | ||

- | * Equality, uninterpreted functions/predicates (EUF); non-linear integer arithmetic; arrays; algebraic data-types (ADTs). | ||

- | * Proof generation and Craig interpolation for all supported theories. | ||

- | * Free variables and triggers and e-matching to handle quantifiers. | ||

- | |||

- | * Input formats: native language of Princess, SMT-LIB 2, and TPTP (FOF/TFF/CNF, see details). | ||

- | |||

- | Princess runs on any platform that provides a Java runtime environment (version 1.5 or higher). There is a convenient API for programmatic use from Scala applications. This API can also be used to integrate Princess in Java applications, although this is somewhat less convenient (for instance see the wrapper used in Bixie, or the JavaSMT library) | ||

- | |||

- | * License: LGPL v2.1 or later | ||

- | * Web site: http://www.philipp.ruemmer.org/princess.shtml | ||

- | |||