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.2.tar.gz sha256=cb86019f69ef19a1742fa3a54fba2415c45fba99bd05767d79fa9b81c17d4290 md5=ef9803cfb67f6ed1fce23853030472f1 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.2/opam |
No package is dependent
