zipperposition

AuthorSimon Cruanes
Homepagehttps://github.com/c-cube/zipperposition
Issue Trackerhttps://github.com/c-cube/zipperposition/issues
Tagslogic, unification, term, superposition and prover
Maintainersimon.cruanes@inria.fr
Dependencies
&base-bytes
base-unix
containers>= 1.0
menhir
msat>= 0.5
ocamlfind
sequence>= 0.4
tip-parser
zarith
Optional dependencies
qcheck
Availableocaml-version >= "4.02.3"
PublishedSep 1, 2017
Source [http] https://github.com/c-cube/zipperposition/archive/1.2.tar.gz
ef9803cfb67f6ed1fce23853030472f1
StatisticsInstalled once last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/zipperposition/zipperposition.1.2/opam

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.

No package is dependent