package zipperposition
A fully automatic theorem prover for typed first-order and beyond.
Install
Dune Dependency
Authors
Maintainers
Sources
1.4.tar.gz
sha256=70fef44612c49b5c4b490a02ffcaff7ab111317a926d665757f0c133a1333b7d
md5=fdd087327b584dbd661172a5fde55a04
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.
Dependencies (9)
-
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.03.0"
Dev Dependencies
None
Used by
None
Conflicts (1)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page