GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages
EPROOF(1) User Commands EPROOF(1)

eproof - manual page for eproof eproof

eproof [ options] <file1> ...

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 options.
In particular, eproof will automatically do a close approximation of 'the right thing' (tm) with the options describing input- and output formats.

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

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.

Copyright © 1998-2009 by Stephan Schulz, schulz@eprover.org
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
January 2019 eproof eproof

Search for    or go to Top of page |  Section 1 |  Main Index

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.