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 |
---|---|
Author | Simon Cruanes |
Published | |
Homepage | https://www.rocq.inria.fr/deducteam/Zipperposition/index.html |
Issue Tracker | https://github.com/c-cube/zipperposition/issues |
Maintainer | simon.cruanes@inria.fr |
Dependencies | |
Optional dependencies | |
Conflicts |
|
Source [http] | https://github.com/c-cube/zipperposition/archive/1.0.tar.gz md5=48b8a8319663b6520622fe23f24fc073 |
Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.0/opam |
No package is dependent