package archsat
A first-order theorem prover with formal proof output
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.tar.gz
md5=14a97e6f88adc863d2f208b5563209f6
sha512=d1a2aa3b29de82b9954f926ef8771d391e5028c254b8a63d6ca7472cc063becd6adca2056f9599e6ae176d2364a0efeed082858a97cd6bcb1ebbb818d2ffba7b
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)
-
uutf
>= "1.0" - uucp
-
spelll
>= "0.3" -
iter
>= "0.5" -
mtime
< "1.4.0" - gen
- ocamlgraph
- zarith
-
cmdliner
>= "0.9.8" -
containers
>= "2.0" & < "3.0" -
msat
>= "0.7" & < "0.8" -
dolmen
>= "0.4" & < "0.5" -
ocamlbuild
build -
ocamlfind
build -
ocaml
>= "4.07.0"
Dev Dependencies (1)
-
qcheck
with-test & >= "0.8"
Used by
None
Conflicts
None
On This Page