zipperposition

A fully automatic theorem prover for typed first-order and beyond.
Description

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.

Install
logic unification term superposition prover
Documentation github.com Edit opam file
Published
02 Sep 2017
Authors
Maintainers
Sources
1.2.tar.gz
md5=ef9803cfb67f6ed1fce23853030472f1
Dependencies
tip-parser < "0.4"
menhir build
msat >= "0.5" & < "0.8"
sequence >= "0.4" & < "1.0"
containers >= "1.0" & < "2.0"
zarith < "1.8"
base-unix
base-bytes
ocamlfind build
ocaml >= "4.02.3"
Reverse Dependencies
Conflicts
logtk