1E_DEDUCTION_SERVER(1)            User Commands           E_DEDUCTION_SERVER(1)
2
3
4

NAME

6       e_deduction_server  - manual page for e_deduction_server 2.6-DEBUG Flo‐
7       ral Guranse
8

DESCRIPTION

10       e_deduction_server 2.6-DEBUG "Floral Guranse"
11
12              Usage: e_deduction_server -p <port> [options] [files]
13
14              The E deduction server offers deduction services based on  local
15              or
16
17              uploaded axiom sets via network. See README.server.
18

OPTIONS

20       -h
21
22       --help
23
24              Print a short description of program usage and options.
25
26       -V
27
28       --version
29
30              Print the version number of the prover. Please include this with
31              all bug reports (if any).
32
33       -v
34
35       --verbose[=<arg>]
36
37              Verbose comments on the progress of the  program.  This  differs
38              from  the  output level (below) in that technical information is
39              printed to stderr, while the output level determines which logi‐
40              cal  manipulations  of  the  clauses  are printed to stdout. The
41              short form or the long form without  the  optional  argument  is
42              equivalent to --verbose=1.
43
44       -p <arg>
45
46       --port=<arg>
47
48              The  port on which the server will receive connections. Only ef‐
49              fective when interactive mode is on. If not  given  stdin/stdout
50              will be used.
51
52       -s
53
54       --silent
55
56              Equivalent to --output-level=0.
57
58       -l <arg>
59
60       --output-level=<arg>
61
62              Select  an  output level, greater values imply more verbose out‐
63              put. Level 0 produces nearly no output, level 1 will output each
64              clause as it is processed, level 2 will output generating infer‐
65              ences, level 3 will give a full protocol including rewrite steps
66              and  level 4 will include some internal clause renamings. Levels
67              >= 2 also imply PCL2 or TSTP formats  (which  can  be  post-pro‐
68              cessed with suitable tools).
69
70       -w <arg>
71
72       --wtc-limit=<arg>
73
74              Set the global wall-clock limit for each batch (if any).
75
76       -L <arg>
77
78       --lib=<arg>
79
80              Set the axioms library directory of the server.
81

REPORTING BUGS

83       Report  bugs  to <schulz@eprover.org>. Please include the following, if
84       possible:
85
86       * The version of the package as reported by eprover --version.
87
88       * The operating system and version.
89
90       * The exact command line that leads to the unexpected behaviour.
91
92       * A description of what you expected and what actually happend.
93
94       * If possible all input files necessary to reproduce the bug.
95

97       Copyright 1998-2021 by Stephan Schulz, schulz@eprover.org,  and  the  E
98       contributors (see DOC/CONTRIBUTORS).
99
100       This  program  is  a part of the distribution of the equational theorem
101       prover E. You can find the latest version of the E distribution as well
102       as additional information at http://www.eprover.org
103
104       This program is free software; you can redistribute it and/or modify it
105       under the terms of the GNU General Public License as published  by  the
106       Free  Software Foundation; either version 2 of the License, or (at your
107       option) any later version.
108
109       This program is distributed in the hope that it  will  be  useful,  but
110       WITHOUT  ANY  WARRANTY;  without  even  the  implied  warranty  of MER‐
111       CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  General
112       Public License for more details.
113
114       You should have received a copy of the GNU General Public License along
115       with this program (it should be contained in the top level directory of
116       the  distribution in the file COPYING); if not, write to the Free Soft‐
117       ware  Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,   MA
118       02111-1307 USA
119
120       The original copyright holder can be contacted via email or as
121
122       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
123       buehlplatz 41 70178 Stuttgart Germany
124
125
126
127e_deduction_server 2.6-DEBUG FloraJlanGuuarrayns2e022            E_DEDUCTION_SERVER(1)
Impressum