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
- Published
-
29 Jul 2016
- Authors
-
- Maintainers
-
Sources
Dependencies
msat
>= "0.3" & < "0.4"
sequence
>= "0.4" & < "0.9"
containers
> "0.16" & < "1.0"
ocamlfind
build
ocaml
>= "4.02.3"
Reverse Dependencies