zipperposition

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

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.

Install
logic unification term superposition prover
Documentation www.rocq.inria.fr Edit opam file
Published
29 Jul 2016
Authors
Maintainers
Sources
1.0.tar.gz
md5=48b8a8319663b6520622fe23f24fc073
Dependencies
num
msat >= "0.3" & < "0.4"
oasis
oclock
gen
sequence >= "0.4" & < "0.9"
containers > "0.16" & < "1.0"
zarith
base-unix
base-bytes
ocamlfind build
ocaml >= "4.02.3"
Reverse Dependencies
Conflicts
sequence >= "0.9"
containers >= "1.2"