package archsat

  1. Overview
  2. No Docs
An first-order theorem prover with formal proof output

Install

Dune Dependency

Authors

Maintainers

Sources

v1.0.tar.gz
md5=15c709d42486ee4ca71134dd064ee19e
sha512=7a4f40caf05ba633840cdf425a205b96d7274ace5ef43e8a7b54d8ffdbb75d066692a52935faa58d7a8c764ee02494f43e4dcf1ea36aa08426ab5ef60620c412

Description

Archsat is an experimental SMT/McSat solver, aimed at solving first-order problems. Archsat integrates Tableau theory, superposition, and Rewriting into an McSat core.

Archsat currently features builtin support for equality, uninterpreted functions and predicates, as well as rewriting. Additionally, whenever it finds a proof, it is able to export that proof to various formal proof formats: coq proof script, coq proof term, dedukti proof term.

Dependencies (15)

  1. uutf >= "1.0"
  2. uucp
  3. spelll <= "0.2"
  4. sequence >= "0.5"
  5. mtime
  6. gen
  7. ocamlgraph
  8. zarith
  9. cmdliner >= "0.9.8"
  10. containers >= "2.0"
  11. msat >= "0.7" & < "0.8"
  12. dolmen >= "0.4"
  13. ocamlbuild build
  14. ocamlfind build
  15. ocaml >= "4.04.0"

Dev Dependencies (1)

  1. qcheck with-test & >= "0.8"

Used by

None

Conflicts

None