NAME

SYNOPSIS

DESCRIPTION

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.

OPTIONS

-h

--help

Print a short description of program usage and options.

--version

Print the version numbers of eprover and epclextract used by this instance of eproof. Please include this with all bug reports (if any).

--proof-time-unlimited

If eprover succeeds within the overall timelimit, don't stop epclextract due to timeout.

REPORTING BUGS

* 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.

COPYRIGHT

You can find the latest version of E and additional information at http://www.eprover.org

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program (it should be contained in the top level directory of the distribution in the file COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

The original copyright holder can be contacted as

Stephan Schulz (I4) Technische Universitaet Muenchen Institut fuer Informatik Boltzmannstrasse 3 85748 Garching bei Muenchen Germany