Design of a proof repository architecture
Michael Franssen, Mark van den Brand · 2009
In this paper, we introduce a proof repository architecture to build a library of proofs for first-order theorems constructed by several theorem provers. The architecture is not fixed as such, but is configured by the user. It consists of three types of components, that allow us to connect theorem provers, store proofs and manage the connections between them. These components allow for many setups, like a local database of theorems, an interconnected series of databases of systems, interconnecting many theorem provers, using a theorem prover in a client-server architecture, Software As Service etc.