Publikation
Querying Proofs
David Aspinall; Ewen Denney; Christoph Lüth
In: 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18). International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, March 10-15, Merida, Venezuela, Pages 92-106, Lecture Notes in Computer Science (LNCS), Vol. 7180, Springer Verlag, Berlin Heidelberg, 2012.
Zusammenfassung
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.