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