Querying Proofs

David Aspinall, Ewen Denney, Christoph Lüth

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We motivate and introduce a query language PrQL designed for inspecting machine representations of proofs. PrQL natively supports hiproofs which express proof structure using hierarchical nested labelled trees. The core language presented in this paper is locally structured, with queries built using recursion and patterns over proof structure and rule names. We define the syntax and semantics of locally structured queries, demonstrate their power, and sketch some implementation experiments.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings
EditorsNikolaj Bjørner, Andrei Voronkov
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Print)978-3-642-28716-9
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Querying Proofs'. Together they form a unique fingerprint.

Cite this