Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

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

home | help