eproof

EPROOF(1)                        User Commands                       EPROOF(1)



NAME
       eproof - manual page for eproof eproof

SYNOPSIS
       eproof [options] <file1> ...

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

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



eproof eproof                      July 2015                         EPROOF(1)