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 for integers and rationals, higher-order, induction). 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.4.tar.gz sha256=70fef44612c49b5c4b490a02ffcaff7ab111317a926d665757f0c133a1333b7d md5=fdd087327b584dbd661172a5fde55a04 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.4/opam |
No package is dependent
