Skip to content
First-order automated theorem prover based on the tableau method
OCaml TLA Coq Standard ML Makefile Shell Turing
Branch: modulo
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
doc
examples
regression
test
.gitattributes
.gitignore
.gitmodules
.merlin
.svnignore
CCVector.ml
CCVector.mli
LICENSE
Makefile
README
README.md
arith.ml
arith.mli
basics_minimal.dk
cc.dk
checksum.mli
config.mli
configure
configure-for-focalize
coqterm.ml
coqterm.mli
dk_bool.dk
dk_logic.dk
dk_tuple.dk
dkterm.ml
dkterm.mli
enum.ml
enum.mli
eqrel.ml
eqrel.mli
error.ml
error.mli
expr.ml
expr.mli
ext_arith.ml
ext_arith.mli
ext_equiv.ml
ext_equiv.mli
ext_focal.ml
ext_focal.mli
ext_induct.ml
ext_induct.mli
ext_recfun.ml
ext_recfun.mli
ext_tla.ml
ext_tla.mli
extension.ml
extension.mli
globals.ml
globals.mli
heap.ml
heap.mli
index.ml
index.mli
isar_case.ml
isar_case.mli
lexcoq.mli
lexcoq.mll
lexdk.mli
lexdk.mll
lexsmtlib.mli
lexsmtlib.mll
lextptp.mli
lextptp.mll
lexzen.mli
lexzen.mll
linear_ari_tptp.list
llproof.ml
llproof.mli
lltocoq.ml
lltocoq.mli
lltodk.ml
lltodk.mli
lltoisar.ml
lltoisar.mli
log.ml
log.mli
main.ml
main.mli
misc.ml
misc.mli
mlproof.ml
mlproof.mli
mltoll.ml
mltoll.mli
namespace.ml
namespace.mli
node.ml
node.mli
parsecoq.mly
parsedk.mly
parsetptp.mly
parsezen.mly
phrase.ml
phrase.mli
print.ml
print.mli
printBox.ml
printBox.mli
progress.ml
progress.mli
prove.ml
prove.mli
rewrite.ml
rewrite.mli
run
simplex.ml
simplex.mli
smtlib.ml
smtlib.mli
smtlib_syntax.ml
smtlib_syntax.mli
smtlib_util.ml
smtlib_util.mli
step.ml
step.mli
tptp.ml
tptp.mli
typer.ml
typer.mli
typesmtlib.ml
typesmtlib.mli
typetptp.ml
typetptp.mli
version.ml
version.mli
versionnum.ml
versionnum.mli
watch.ml
watch.mli
zen.dk
zenon.ml
zenon.mli
zenon.spec
zenon.v
zenon_arith.v
zenon_arith_reals.v
zenon_coqbool.v
zenon_equiv.v
zenon_focal.dk
zenon_focal.v
zenon_induct.v

README.md

ZENON

Zenon is a first-order automated theorem prover based on the tableau method. It is used in the FoCaLiZe project.

COPYRIGHT

Under the new BSD License (see the file LICENSE for details)

INSTALLATION

DEPENDENCIES

This depends on:

  • OCaml >= 4.02.1
  • ZArith >= 1.3
  • Coq >= 8.0
  • Graphviz (optional)

COMPILATION

In order to compile, use :

./configure
make

This should make available to you the zenon executable in the root directory. If you want to install the binary, then issue the following command:

make install

USAGE

TPTP LIBRARY

In order to use zenon on problems from the tptp problem library, be suze to use the -itptp option in order to set the corret input parser. A standard use of zenon would then look like this:

./zenon -itptp -max-time 60s -max-size 1G /path/to/tptp/problem.p

ARITHMETIC

In order to activate the arithmetic extension of zenon, you have to use the -x arith option. You should also use the -k option, in order to activate the arithmetic instantiation search. A usual use of zenon on an arithemtic problem would look like:

./zenon -itptp -max-time 60s -max-size 1G \
      -k -x arith $TPTP/Problems/ARI/ARI001\=1.p

COQ PROOFS

In order to output checkable coq proofs, you have to use the -ocoq option. Additionally, you should use the -context and -opt0 option. A complete execution of zenon and checking of the proof by the coq compiler afterwards would look like the following, assuming that your current working directory is the zenon root directory.

./zenon -itptp -max-time 5s -max-size 1G -k -x arith \
      -ocoq -context -opt0 $TPTP/Problems/ARI/ARI001\=1.p > temp.v
coqc -I ./ temp.v

If no erros are produced, and the coqc command has return code 0, it means everything went well and the proof has been accepted by the coq compiler.

MISC

VERSION NUMBER

The version number starts from scratch fro this extension, but this extension will be merged into the main branch of Zenon sooner or later.

LINEAR ARITHMETIC BENCHMARKS

In the source directory, you will find a file linear_ari_tptp.list, which contains a list of linear problems of the ARI section of the tptp library. These problems only involve linear arithmetic, and do not use the $to_int, $to_rat, $to_real, $is_int or $is_rat functions and predicates. This is the list of files used to benchmark the arithmetic extension of zenon against the princess and beagle automated provers.

CONTACT

Guillaume Bury guillaume.bury@inria.fr

Mohamed Yacine EL HADDADD mohamed-yacine.el-haddad@inria.fr

You can’t perform that action at this time.