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). 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
copied = false, 2000)"
:class="{ 'border-gray-700': !copied, 'text-gray-100': !copied, 'focus:ring-orange-500': !copied, 'focus:border-orange-500': !copied, 'border-green-600': copied, 'text-green-600': copied, 'focus:ring-green-500': copied, 'focus:border-green-500': copied }">
Published
08 Apr 2017
Authors
Maintainers
Sources
1.1.tar.gz
md5=264c113d62f26d184fdb0b4f51a43d98
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"
ocamlfind
build
ocaml
>= "4.02.1"
Reverse Dependencies
None
Conflicts
containers
>= "1.2"