eproof_ram

EPROOF_RAM(1)                    User Commands                   EPROOF_RAM(1)



NAME
       eproof_ram - manual page for eproof_ram PROVER/eproof_ram

SYNOPSIS
       eproof_ram [options] <file1> ...

DESCRIPTION
       eproof

       Eproof_ram is a wrapper around E and epclextract. It will run E with
       output level 4 (full output of all potentially proof-relevant
       inferences) and pipe the output through epclextract to provide a proof
       derivation or a derivation of all clauses in the saturated proof state.

       Eproof_ram will intercept the command line arguments and interpret
       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_ram 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).

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-2011 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_ram PROVER/eproof_ram       July 2015                     EPROOF_RAM(1)