A Semantic Basis for Proof Queries and Transformations

David Aspinall, Ewen Denney, Christoph Lüth

In: Kevin McMillan , Aart Middeldorp , Andrei Voronkov (Hrsg.). Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2013) 19th December 14-19 Stellenbosch South Africa Seiten 53-70 Lecture Notes in Computer Science 8312 Springer 2013.


We extend the query language PrQL, which is designed for inspecting machine representations of proofs, to also allow transformations of these proofs. There are several novel aspects. First, PrQL natively supports hiproofs which express proof structure using hierarchically nested labelled trees, which we claim is a natural way of taming the complexity of huge proofs. Query-driven transformations enable manipulation of this structure, in particular, to transform proofs produced by interactive theorem provers into forms that assist their understanding, or that could be consumed by other tools. In this paper we motivate and define basic transformation operations, using a new abstract denotational semantics of hiproofs and queries. This extends our previous semantics for queries based on syntactic tree representations. We define update operations that add and remove sub-proofs, and manipulate the hierarchy to group and ungroup nodes. We show that these basic operations are well-behaved so can form a sound core for a hierarchical transformation language.


main.pdf (pdf, 355 KB )

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