package zipperposition

  1. Overview
  2. No Docs
Zipperposition is a superposition prover for full first order logic with equality.

Install

www.rocq.inria.fr Edit opam file

Authors

  1. S
    Simon Cruanes

Maintainers

  1. S
    simon.cruanes@inria.fr

Sources

1.0.tar.gz
md5=48b8a8319663b6520622fe23f24fc073

Description

The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces and features many simplification rules and redundancy criteria.

Tags

logic unification term superposition prover

Published: 29 Jul 2016

Dependencies (12)

  1. num
  2. msat >= "0.3" & < "0.4"
  3. oasis
  4. oclock
  5. gen
  6. sequence >= "0.4" & < "0.9"
  7. containers > "0.16" & < "1.0"
  8. zarith
  9. base-unix
  10. base-bytes
  11. ocamlfind build
  12. ocaml >= "4.02.3"

Dev Dependencies

None

Used by

None

Conflicts (2)

  1. sequence >= "0.9"
  2. containers >= "1.2"