forked from eprover/eprover
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.server
112 lines (75 loc) · 2.6 KB
/
README.server
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
Short Installation
------------------
This assumes that you have GNU tar, sh and gawk in your search path!
Simplest installation:
> tar -xzf E.tgz
> cd E
> ./configure
> make
Starting The Server
-------------------
From the root directory of E
> ./PROVER/e_deduction_server ./PROVER/eprover -p <port> -L <server_library>
- Replace the <port> with the port you want the server to start
listening to. The port should be an unused port, typically in the
non-reserved "registered port" section. If in doubt, try 2705.
- Replace the <server_library> with a directory that contains the
server-side libraries that you want to be availabe to clients. This
argument is optional. If you want to test this feature, we have
added some axioms sets. Use './EXAMPLES/AXIOMS'.
The conrete example with the recommended values would be
> ./PROVER/e_deduction_server ./PROVER/eprover -p 2705 -L ./EXAMPLES/AXIOMS
Starting The Client
-------------------
From the root directory of E
> ./PYTHON/enetcat.py localhost <port>
- Replace the <port> with the port you started your server with.
Example Commands
---------------
(Note: Capitalization is significant)
LIST
ADD axiom_set1
fof(inp1,axiom,(subclass(a,b))).
fof(inp2,axiom,(subclass(b,c))).
GO
ADD axiom_set2
fof(inp3,axiom,![X,Y,Z]:((subclass(X,Y) & subclass(Y,Z)) => subclass(X,Z))).
GO
STAGE axiom_set1
LIST
STAGE axiom_set2
RUN job1
fof(inp4,conjecture,(subclass(a,c))).
GO
UNSTAGE axiom_set2
REMOVE axiom_set2
DOWNLOAD axiom_set1
RUN job2
fof(inp4,conjecture,(subclass(a,c))).
GO
Example session with server-side axioms:
-----------------------------------------
LIST
LOAD CSR002+2.ax
STAGE CSR002+2.ax
RUN job3
fof(query75,conjecture,
( mtvisible(c_patterndetectormt)
=> genls(c_tptpcol_16_130933,c_tptpcol_15_130931) )).
GO
QUIT
Available Commands
------------------
Note : Block commands that are in the form of "COMMAND <NAME> ... GO" should have the
"COMMAND <NAME>" and GO each on a seperate line on their own and the block should be
in between. Check the above examples.
- ADD <NAME> ... GO : Uploads a new axiom set with the name <NAME>.
- LOAD <NAME> : Loads a server-side axiom set with the name <NAME>.
- STAGE <NAME> : Stages the axiom set <NAME>.
- UNSTAGE <NAME> : Unstages the axiom set <NAME>.
- REMOVE <NAME> : Removes the axiom set <NAME> from the memory.
- DOWNLOAD <NAME> : Prints the axiom set <NAME>.
- RUN <NAME> ... GO : Runs a job with the name <NAME>.
- LIST : Prints the status of the axiom sets.
- HELP : Prints the help message.
- QUIT : Closes the connection with the server.