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.2007@m4x.org |
| Dependencies |
|
| Source [http] | https://github.com/c-cube/zipperposition/archive/1.5.tar.gz sha256=b85b710cb7549aa5cc4ebb12adf14ddda60f66c439ab336535ecafc9dc4ab952 md5=1727ad8ea0920b584307cabb2de45e0b |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.5/opam |
No package is dependent
