Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009, Montreal, Canada, August 3, 2009) |
| Place of Publication | New York NY |
| Publisher | Association for Computing Machinery, Inc |
| Pages | 19-23 |
| ISBN (Print) | 978-1-60558-954-1 |
| DOIs | |
| Publication status | Published - 2009 |
Publication series
| Name | ACM International Conference Proceeding Series |
|---|---|
| Volume | 429 |
Fingerprint Dive into the research topics of 'Design of a proof repository architecture'. Together they form a unique fingerprint.
Cite this
Franssen, M. G. J., & Brand, van den, M. G. J. (2009). Design of a proof repository architecture. In Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009, Montreal, Canada, August 3, 2009) (pp. 19-23). (ACM International Conference Proceeding Series; Vol. 429). Association for Computing Machinery, Inc. https://doi.org/10.1145/1735813.1735817