Design of a proof repository architecture

M.G.J. Franssen, M.G.J. Brand, van den

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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 languageEnglish
Title of host publicationProceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009, Montreal, Canada, August 3, 2009)
Place of PublicationNew York NY
PublisherAssociation for Computing Machinery, Inc
Pages19-23
ISBN (Print)978-1-60558-954-1
DOIs
Publication statusPublished - 2009

Publication series

NameACM International Conference Proceeding Series
Volume429

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