Zipperposition

Zipperposition is a first-order prover written in OCaml. It is based on the superposition calculus. It is developped by Simon Cruanes and available under the BSD-3 license.

The main page of the prover is on github. The master branch should be relatively stable. Release archives can be found here but you will still need to install the dependencies.

Please note that Zipperposition is alpha software, and is likely to contain bugs. If you find some, please consider reporting bugs!

Usage

The only supported input format is currently TPTP (the basic syntax of FOF and TFF1).

$ zipperposition -help

To run zipperposition on a TPTP problem, just type

$ zipperposition foobar.p

Zipperposition now supports linear integer arithmetic (in the TFF format) using the flag -arith, and can handle structural induction for types declared as such. For instance, natural numbers:

tff(_, type, nat : $tType, inductive(succ,zero)).

Take a look at example problems in pelletier_problems/ and examples/.

Installation

Via opam

The recommended way to install Zipperposition is through opam. Deducteam has its own opam repository whose adress is https://scm.gforge.inria.fr/anonscm/git/opam-deducteam/opam-deducteam.git . You need to have GMP (with headers) installed (it's not handled by opam). Once you installed GMP and opam, type:

$ opam repository add deducteam https://scm.gforge.inria.fr/anonscm/git/opam-deducteam/opam-deducteam.git

$ opam install zipperposition

To upgrade to more recent versions:

$ opam update

$ opam upgrade

From sources

It may not be very simple to compile Zipperposition from sources. Please check the README.md file in the release page's archives.

Parent page


Home, Members, Software, Seminars

logo inria logo deducteam