TY - GEN
T1 - Design of a proof repository architecture
AU - Franssen, M.G.J.
AU - Brand, van den, M.G.J.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
U2 - 10.1145/1735813.1735817
DO - 10.1145/1735813.1735817
M3 - Conference contribution
SN - 978-1-60558-954-1
T3 - ACM International Conference Proceeding Series
SP - 19
EP - 23
BT - Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009, Montreal, Canada, August 3, 2009)
PB - Association for Computing Machinery, Inc.
CY - New York NY
ER -