FreeBSD Manual Pages
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 re- ports (if any). --proof-time-unlimited If eprover succeeds within the overall timelimit, don't stop ep- clextract 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 (C) 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 MER- CHANTABILITY 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 Soft- ware 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 In- formatik Boltzmannstrasse 3 85748 Garching bei Muenchen Germany eproof eproof August 2020 EPROOF(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | REPORTING BUGS | COPYRIGHT
Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=eproof&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>