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.
|Title of host publication||Logic for Programming, Artificial Intelligence, and Reasoning|
|Subtitle of host publication||18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings|
|Editors||Nikolaj Bjørner, Andrei Voronkov|
|Number of pages||15|
|Publication status||Published - 2012|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|