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 sha256=287a24ec7109b00ff56b97cabce15f3ce6c130fe1f4fb52cb7bec2b64c9e2917 md5=48b8a8319663b6520622fe23f24fc073 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.0/opam |
No package is dependent
