zipperpositionversion

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.

Tags logic unification term superposition prover
AuthorSimon Cruanes
Published
Homepagehttps://www.rocq.inria.fr/deducteam/Zipperposition/index.html
Issue Trackerhttps://github.com/c-cube/zipperposition/issues
Maintainersimon.cruanes@inria.fr
Dependencies
Optional dependencies
Conflicts
Source [http] https://github.com/c-cube/zipperposition/archive/1.0.tar.gz
md5=48b8a8319663b6520622fe23f24fc073
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.0/opam
No package is dependent