package zipperposition

  1. Overview
  2. Docs
A fully automatic theorem prover for typed first-order and beyond.

Install

Dune Dependency

github.com Edit opam file Versions (9)

Authors

  1. S
    Simon Cruanes

Maintainers

  1. S
    simon.cruanes@inria.fr

Sources

1.1.tar.gz
md5=264c113d62f26d184fdb0b4f51a43d98

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.

Tags

logic unification term superposition prover

Published: 08 Apr 2017

Dependencies (12)

  1. num
  2. tip-parser < "0.4"
  3. menhir build
  4. msat >= "0.5" & < "0.8"
  5. oclock
  6. sequence >= "0.4" & < "1.0"
  7. containers >= "1.0" & < "2.0"
  8. zarith < "1.8"
  9. base-unix
  10. base-bytes
  11. ocamlfind build
  12. ocaml >= "4.02.1"

Dev Dependencies

None

Used by

None

Conflicts (1)

  1. containers >= "1.2"