zipperpositionversion
A fully automatic theorem prover for typed first-order and beyond.
Zipperposition is intended to be a superposition prover for full first order logic, plus some extensions (datatypes, recursive functions, arithmetic). The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces or graphviz files for nice graphical display.
| Tags | logic unification term superposition prover |
|---|---|
| Author | Simon Cruanes |
| Published | |
| Homepage | https://github.com/c-cube/zipperposition |
| 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.1.tar.gz sha256=17cb74397e966cb857bd3cadbddebd74a6921359cf24b4b898211312c5a059b9 md5=264c113d62f26d184fdb0b4f51a43d98 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.1/opam |
No package is dependent
