We describe a system o ering deduction (over a xed but exible background theory) as a service, provided to a client via a network connection. The deduction server maintains the (potentially) large background knowledge base in a form that makes processing of individual conjectures and queries easy and avoids most of the overhead of reading and analyzing large background theories for each individual job. The client connects to the server, can update the background theory by adding and removing client-side or server-side axiom sets, and ask the server to solve proof problems on its behalf. This o ers several bene ts: Preprocessing costs can be amortized over multiple proof attempts. The user can be isolated from the complexities of a locally installed ATP system (and indeed locally maintained knowledge bases). Finally, the deduction server can easily o er true strategy parallelism even with sequential back-end theorem provers. This paper describes the architecture, the communication protocol, and the implementation of a deduction server based on E. First experimental results demonstrate the feasibility of the technology and the performance bene ts possible with this approach.
Classical automated theorem proving has long been concerned with solving individual problems, one at a time.
Moreover, problems have often been hand-optimized, either to solve a particular mathematical question, or
to analyze and demonstrate the performance of di erent theorem proving strategies (see e.g. [
However, in recent years, theorem provers have been used in a very di erent setting. Users have developed
large theories, either by large-scale manual coding of knowledge as in Cyc [
In these newer use cases, the theorem prover proves and reproves many di erent theorems over a large and
mostly static background theory. Typically, the background theory has thousands to millions of axioms, only a
small fraction of which is used for any given proof. Premise selection techniques [
In this paper, we suggest a di erent paradigm. Deduction, over a xed but exible base theory, is o ered as a network service. The deduction server maintains a knowledge base of several pre-loaded background axiomatization. The user can connect to the server, select speci c parts of the knowledge base, add additional assumptions, and then request a proof from the server. The server combines the pre-loaded and pre-indexed background theory with the new formulas provided by the user, runs several premise selection strategies to generate ATP problems, and runs several ATP instances with di erent heuristics to try to solve the problem. If one of the server processes nds a proof, it is handed back to the client.
This approach has a number of advantages. First, the cost of loading and pre-processing the large background theory is amortized over many di erent proof problems. Proofs to individual problems are often found fast and with low latency. The user can prepare and issue queries from a local desktop, while the deduction server can be shared by several users and run on powerful server hardware. Indeed, the user does not even need to know how to install or invoke ATP systems, since the server can be centrally installed and maintained.
We have developed a suitable communication protocol and implemented a deduction server based on the
theorem prover E[
The system is available at http://www.eprover.eu/E-eu/DedServer.html, and will become part of future distributions of E. 2 2.1
The deduction server is the central component for o ering Deduction as a Service. It maintains the current state of the knowledge base, accepts connections from clients, reads and processes their requests, runs deduction jobs on behalf of the clients, and transmits the results back to the client. The main architectural components of the server are the knowledge base, the TCP interface, the axiom lter, and the execution module.
At start-up, the server starts listening on a user-speci ed port for incoming TCP connections. Whenever a client tries to connect to the server on that port, a process is forked from the main process to serve the client. The server can thus handle several di erent connections at the same time, and each client is completely isolated from other clients connected to the server.
The client interacts with the server using the protocol speci ed in section 2.3. The server implements a typical
read-execute-print loop, accepting commands from the client, executing them, and sending the results back to
the client. The client can upload axiom sets, remove them, and query the server for proofs and answers (i.e.
instantiations of variables that make an existentially quanti ed query formula true [
Whenever the client uploads a set of axioms, the server parses the axioms, adds them to various indexes useful for axiom selection/pruning methods, and adds them to the in-memory knowledge base. However, these uploaded axiom sets will not automatically be used by each proof attempt, but only when the client has also activated (or staged ) the particular set in the current session. Thus, the server maintains a pre-indexed, ready-to-use library of axiom sets. In addition to axiom sets uploaded by the client, the server can also o er access to axiom sets 1As an example, E takes around 54 seconds (on a system with a 4 GHz Intel i7 and a fast SSD) just to parse the TPTP problem CSR073+6.p, a rst-order problem based on OpenCyc with nearly 3.5 million axioms and taking up 480 MB. Indexing for SInE axiom selection takes a further 2 seconds, while more than half of successful proof attempts need less than 1 second. stored in a server-side library on disk. Axioms loaded by the server on start-up are available to all users, while axiom sets added by a user during a session are currently only available in that session.
After the client chooses some axiom sets to be used in the proof search, it can start querying the server. The query consists of optional query-speci c axioms and a conjecture. These additional formulas are discarded immediately after the query has been processed. The server adds the new axiom set to the currently staged part of the knowledge base and hands the problem to the axiom lter. The axiom lter module applies one or multiple di erent relevancy pruning strategies to the extended knowledge base. Each of the pruning strategies produces one much smaller proof problem. The pruned problems are passed to the execution module, which starts several instances of E in parallel and monitors their success or failure. Whenever one of the running E instances nds a proof for the conjecture, the other instances are stopped and the proof is returned back to the user. Currently, all instanced of E use its conventional automatic mode, and rely on the di erent pruning strategies to provide diversity for the proof attempt.
The rough architecture of the deduction server is shown in Figure 1.
The deduction server is written in C and integrated with the E distribution. It uses the E libraries and data types to parse and represent logical formulas, to maintain and process rst order knowledge bases, and to perform axiom selection. 2.2
The E distribution includes a small Python client called \enetcat.py", which can be used to interact with the server. The client is intended as a reference implementation, to demonstrate the interactions with the server and enable other developers to use it as a model for interfacing the server with other systems.
The client requires the address and the port of the deduction server as arguments. It opens a TCP connection to the server and then reads the user's commands from \stdin", communicates them to the server, and prints the output back to \stdout".
In addition to encoding the plain text commands into the distinct length-delimited TCP messages expected by the server, the client o ers two convenience features. First, it o ers command line editing. Secondly, it locally expands TPTP style include commands for formula sets to be uploaded to the server. This makes uploading of even large axioms sets plausible and convenient.
The current client is tailored towards command-line users. However, the protocol is simple enough to be implemented in a few lines of code in nearly any modern programming language, making other clients, in particular a web-based client, easily possible. 2.3
As mentioned before, the communication between the server and the client is done over TCP to ensure reliability. TCP messages between the server and the client are encoded in a way to ease the communication between them. Each TCP messages starts with 4 bytes containing the length of the messages, including those 4 bytes, followed by the actual message. The commands themselves are plain, human-readable ASCII text.
We describe the protocol for communication between the server and the client using a running example. We assume that the connection has already been established and all messages are encoded as described in the previous paragraph.
The rst section of the session uploads two small axiom sets to the server. 1 ADD axiom_set1 2 fof(inp1,axiom,(subclass(a,b))). 3 fof(inp2,axiom,(subclass(b,c))). 4 GO 5 >205 ok : added 6 7 ADD axiom_set2 8 fof(inp3,axiom,((subclass(X,Y) & subclass(Y,Z)) => subclass(X,Z))). 9 GO 10 >205 ok : added
Each of the \ADD . . . GO" blocks upload one named set of axioms to the system. Axioms uploaded are parsed and stored in the memory of the server, but are not automatically included in future proof attempts. The server responds with the success status of each command's execution. 1 STAGE axiom_set1 2 >201 ok : staged 3 4 LIST 5 >Staged : 6 > axiom_set1 7 >Unstaged : 8 > axiom_set2 9 >On Disk : 10 > test.p 11 >200 ok : success 12 13 STAGE axiom_set2 14 >201 ok : staged
To select axiom sets for future proof attempts, we use the \STAGE" command. It marks the named axiom set as active for later proof attempts. The \LIST" command provides the status of all axiom sets currently known to the server. Possible states are Staged, Unstaged (but in memory and pre-indexed for axiom selection), and On Disk, i.e. known to the server, but not loaded or indexed. Server-side axiom sets can be loaded into the server's memory using the \LOAD" command. 1 RUN job1 2 fof(inp4,conjecture,(subclass(a,c))). 3 GO 4 # Pid: 27988 5 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S0Y 6 # and selection function SelectMaxLComplexAvoidPosPred. 7 # 8 # Preprocessing time : 0.010 s 9 # Presaturation interreduction done 10 11 # Proof found! 12 # SZS status Theorem 13 # SZS output start CNFRefutation. 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 # User time : 0.008 s 52 # System time : 0.002 s 53 # Total time : 0.010 s 54 # Maximum resident set size: 2838528 pages 55 56 # Processing finished for job1 57 58 200 ok : success fof(c_0_0, axiom, (((subclass(X1,X2)&subclass(X2,X3))=>subclass(X1,X3))), file('/var/folders/__/ss_kh09s5_l9s1twdz7k5y900000gn/T//epr_VKSv9K', i_0_3)). fof(c_0_1, conjecture, (subclass(a,c)), file('/var/folders/__/ss_kh09s5_l9s1twdz7k5y900000gn/T//epr_VKSv9K', i_0_4)). fof(c_0_2, axiom, (subclass(b,c)), file('/var/folders/__/ss_kh09s5_l9s1twdz7k5y900000gn/T//epr_VKSv9K', i_0_2)). fof(c_0_3, axiom, (subclass(a,b)), file('/var/folders/__/ss_kh09s5_l9s1twdz7k5y900000gn/T//epr_VKSv9K', i_0_1)). fof(c_0_4, plain, (((~subclass(X1,X2)|~subclass(X2,X3))|subclass(X1,X3))), inference(fof_nnf,[status(thm)],[c_0_0])). fof(c_0_5, negated_conjecture, (~subclass(a,c)), inference(fof_simplification,[status(thm)],[inference(assume_negation, [status(cth)],[c_0_1])])). cnf(c_0_6, plain, (subclass(X1,X2)|~subclass(X3,X2)|~subclass(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_4])). cnf(c_0_7, plain, (subclass(b,c)), inference(split_conjunct, [status(thm)],[c_0_2])). cnf(c_0_8, negated_conjecture, (~subclass(a,c)), inference(split_conjunct,[status(thm)],[c_0_5])). cnf(c_0_9, plain, (subclass(X1,c)|~subclass(X1,b)), inference(spm,[status(thm)],[c_0_6, c_0_7])). cnf(c_0_10, plain, (subclass(a,b)), inference(split_conjunct, [status(thm)],[c_0_3])). cnf(c_0_11, negated_conjecture, ($false), inference(cn,[status(thm)], [inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_8, c_0_9]), c_0_10])]), ['proof']). # SZS output end CNFRefutation.
After staging the needed axioms, we can start running a job with \RUN . . . GO" block. Formulas introduced in the RUN command block are used only temporally for this particular job, and are discarded after its termination. These formulas typically contain the conjecture, but can also include additional axioms and assumptions. If the server succeeds in proving the conjecture, it provides back the logical status of the query, and can also include a proof object. 1 UNSTAGE axiom_set2 CSR025+6.p CSR026+6.p CSR027+6.p CSR028+6.p CSR029+6.p CSR030+6.p CSR031+6.p CSR032+6.p CSR033+6.p CSR034+6.p CSR035+6.p CSR036+6.p CSR037+6.p CSR038+6.p CSR039+6.p CSR040+6.p CSR041+6.p CSR042+6.p CSR043+6.p CSR044+6.p CSR045+6.p CSR046+6.p CSR047+6.p CSR048+6.p CSR049+6.p CSR050+6.p CSR051+6.p CSR052+6.p CSR053+6.p CSR054+6.p CSR055+6.p CSR056+6.p CSR057+6.p CSR058+6.p CSR059+6.p CSR060+6.p CSR061+6.p CSR062+6.p CSR063+6.p CSR064+6.p CSR065+6.p CSR066+6.p CSR067+6.p CSR068+6.p CSR069+6.p CSR070+6.p CSR071+6.p CSR072+6.p CSR073+6.p CSR074+6.p CSR111+6.p
Axiom sets can also be \UNSTAGE"d or \REMOVE"d completely from the system. Axiom sets can be retrieved from the server using the \DOWNLOAD" command. The example shows how we remove one of the axiom sets and re-run the job. Without the necessary axioms, the proof is not found. 3
For the experimental evaluation, we selected a set of large problems with a common axiomatization from the
TPTP library [
To illustrate the comparative performance of the service model and the conventional one-problem-at-a-time model, we con gured both versions to run exactly the same problems with exactly the same pruning parameters and E's sequential automatic mode. In particular, the server did not employ any strategy parallelism in pruning or search, but rather selected the same search strategy than the stand-alone prover for each a given problem.
The systems were given a time limit of 30 seconds for actual proof search, in addition to the time taken for parsing and axiom selection for the standalone version (about 110 seconds per problem on this hardware, with some variation). Memory was limited to 1024MB. Tests were performed on a virtualized server with 8 2.6 GHz Intel CPUs, of which only one was e ectively utilized by our test setup. With this con guration, both setups solved 41 of the 51 problems.
We recorded the time taken after 5, 10, 20, 30, 40 and all 51 problems.
The results in Figure 3 show the di erence between the single strategy server mode and the conventional prover. The gure shows the accumulated wall-clock time over the number of problems for which a proof was attempted. In the conventional case, the prover has to parse and index the axiom set for each proof attempt. In the deduction server, the axioms are parsed and indexed for axiom selection only once. The are then kept in the server's memory and multiple queries can be executed against this axiom set. Thus, the pre-processing time of each problem in the single strategy server mode is amortized over multiple runs. 4
We have described the rst implementation of a Deduction Server and have introduced a communication protocol that supports remote reasoning over largely xed but exible domains as a service. Our results shows that the deduction server, even if con gured for identical pruning and search strategies, improves the run time for sets of related problems by a signi cant amount, due to the amortization of costs for parsing and the indexing needed for axiom selection. This clearly shows that the approach is feasible and has promise even if looking at it only from a performance point of view.
In addition to these performance bene ts, having a formal protocol to communicate with the prover over the net makes integrating it with other applications much easier. Having access to a remotely running prover is a win for those who can't install provers locally, e.g. for OS compatibility issues or due to insu cient local computing resources.
Future work includes improved multi-user support, in particular controlling both access, but also the resources, such as CPU time and memory, allocated for each user. Another important step would be the integration of multiple deduction systems in the back-end, to improve overall performance. This would o er a single interface to potentially very diverse deduction systems.
Finally, the Deduction Server can be extended to a cluster of servers, to o er real scalable deduction as a service. In the simplest version, a single head node accepts and processes user commands, pre-processes the problems, and distributes the deduction jobs to di erent servers. An even more scalable version would maintain di erent user sessions with the current axiomatization on dedicated machines, so that axiom selection can also be distributed. [20] Andrzej Trybulec and Howard A. Blair. Computer assisted reasoning with MIZAR. In Proc. of the 9th IJCAI, Los Angeles, volume 85, pages 26{28. Morgan Kaufmann, 1985.