zipperposition

AuthorSimon Cruanes
Homepagehttps://www.rocq.inria.fr/deducteam/Zipperposition/index.html
Issue Trackerhttps://github.com/c-cube/zipperposition/issues
Tagslogic, unification, term, superposition and prover
Maintainersimon.cruanes@inria.fr
Dependencies
&base-bytes
base-unix
containers0.16&1.0
gen
msat>= 0.3&0.4
oasis
ocamlfind
oclock
sequence>= 0.4&0.9
zarith
Optional dependencies
|menhir
qcheck
Availableocaml-version >= "4.02.3"
PublishedJul 29, 2016
Source [http] https://github.com/c-cube/zipperposition/archive/1.0.tar.gz
48b8a8319663b6520622fe23f24fc073
StatisticsInstalled 12times in last month.
Edithttps://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