Publication

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) 7180 Springer Verlag Berlin Heidelberg 2012.

Abstract

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.

Projekte

lpar2012.pdf (pdf, 220 KB)

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz