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.

Tags

sat smt solver theorem prover tptp logic smtlib dimacs

Published: 16 Jan 2019

Dependencies (16)

  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. qcheck with-test & >= "0.8"
  14. ocamlbuild build
  15. ocamlfind build
  16. ocaml >= "4.04.0"

Reverse Dependencies

    None

Conflicts

    None
An first-order theorem prover with formal proof output

Install

Documentation failed to build. gforge.inria.fr Edit opam file

Authors

  1. G
    Guillaume Bury

Maintainers

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Sources

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