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
Published
23 Jan 2018
Sources
1.5.tar.gz
md5=1727ad8ea0920b584307cabb2de45e0b
Dependencies
menhir
build & < "20211215"
msat
>= "0.5" & < "0.8"
jbuilder
>= "1.0+beta7"
sequence
>= "0.4"
containers
>= "1.0" & < "3.0"
zarith
< "1.8"
ocaml
>= "4.03.0"
Reverse Dependencies