eproof man page

eproof — manual page for eproof eproof


eproof [options] <file1> ...



Eproof is a wrapper around E and epclextract. It will run E with output level 4 (full output of all potentially proof-relevant inferences) and, in the case of success, automatically run epclextract to provide a proof derivation or a derivation of all clauses in the saturated proof state.

Please note that eproof, unlike most E tools, does not support reading problems from stdin. It will silently assume an empty input from stdin.

Eproof will intercept the command line arguments and interprete certain options as described below. All other options and arguments are passed on to eprover or epclextract, as appropriate. See those tools help pages for the supported options.

In particular, eproof will automatically do a close approximation of 'the right thing' (tm) with the options describing input- and output formats.


Print a short description of program usage and options.
Print the version numbers of eprover and epclextract used by this instance of eproof. Please include this with all bug reports (if any).
If eprover succeeds within the overall timelimit, don't stop epclextract due to timeout.

Reporting Bugs

Report bugs to <schulz@eprover.org>. Please include the following, if possible:

* The version of the package as reported by eprover --version.

* The operating system and version.

* The exact command line that leads to the unexpected behaviour.

* A description of what you expected and what actually happend.

* If possible all input files necessary to reproduce the bug.


February 2018 eproof eproof User Commands