home | help
E_DEDUCTION_SERVER(1)		  User Commands 	   E_DEDUCTION_SERVER(1)

NAME
     e_deduction_server - manual page for e_deduction_server 2.6 Floral Guranse

DESCRIPTION
     e_deduction_server 2.6 "Floral Guranse"

	    Usage: e_deduction_server -p <port> [options] [files]

	    The E deduction server offers deduction services based on local or

	    uploaded axiom sets via network. See README.server.

OPTIONS
     -h

     --help

	    Print a short description of program usage and options.

     -V

     --version

	    Print the version number of the prover. Please include this with all
	    bug reports (if any).

     -v

     --verbose[=<arg>]

	    Verbose  comments  on the progress of the program. This differs from
	    the output level (below) in that technical information is printed to
	    stderr, while the output level determines  which  logical  manipula-
	    tions  of  the  clauses are printed to stdout. The short form or the
	    long form without the optional  argument  is  equivalent  to  --ver-
	    bose=1.

     -p <arg>

     --port=<arg>

	    The  port  on which the server will receive connections. Only effec-
	    tive when interactive mode is on. If not given stdin/stdout will  be
	    used.

     -s

     --silent

	    Equivalent to --output-level=0.

     -l <arg>

     --output-level=<arg>

	    Select  an	output	level, greater values imply more verbose output.
	    Level 0 produces nearly no output, level 1 will output  each  clause
	    as it is processed, level 2 will output generating inferences, level
	    3 will give a full protocol including rewrite steps and level 4 will
	    include  some internal clause renamings. Levels >= 2 also imply PCL2
	    or TSTP formats (which can be post-processed with suitable tools).

     -w <arg>

     --wtc-limit=<arg>

	    Set the global wall-clock limit for each batch (if any).

     -L <arg>

     --lib=<arg>

	    Set the axioms library directory of the server.

REPORTING BUGS
     Report bugs to <schulz@eprover.org>. Please include the following, if  pos-
     sible:

     * 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-2021  by Stephan Schulz, schulz@eprover.org, and the E con-
     tributors (see DOC/CONTRIBUTORS).

     This program is a part of the distribution of the equational theorem prover
     E. You can find the latest version of the E distribution as well  as  addi-
     tional information at http://www.eprover.org

     This program is free software; you can redistribute it and/or modify it un-
     der  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 FIT-
     NESS 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 Foun-
     dation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA

     The original copyright holder can be contacted via email or as

     Stephan  Schulz  DHBW Stuttgart Fakultaet Technik Informatik Rotebuehlplatz
     41 70178 Stuttgart Germany

e_deduction_server 2.6 Floral G... August 2026		   E_DEDUCTION_SERVER(1)

home | help