eproof - manual page for eproof eproof
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
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.
Report bugs to <firstname.lastname@example.org>. Please include the following, if
* 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 © 1998-2009 by Stephan Schulz, email@example.com
You can find the latest version of E and additional information at
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
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