zipperposition

Author Simon Cruanes
Homepage https://www.rocq.inria.fr/deducteam/Zipperposition/index.html
Issue Tracker https://github.com/c-cube/zipperposition/issues
Tags { logic, unification, term, superposition, prover }
Maintainer simon.cruanes@inria.fr
Dependencies
& base-bytes
base-unix
containers 0.16
gen
msat >= 0.3& 0.4
oasis
ocamlfind
oclock
sequence >= 0.4
zarith
Optional dependencies
| menhir
qcheck
Available ocaml-version >= "4.02.3"
Published Jul 29, 2016
Source [http] http://github.com/c-cube/zipperposition/archive/1.0.tar.gz
48b8a8319663b6520622fe23f24fc073
Statistics Installed 14 times in last month.
Edit https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.0/opam

Zipperposition is a superposition prover for full first order logic with equality.

The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces and features many simplification rules and redundancy criteria.

No package is dependent