Publication
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, Pages 53-70, Lecture Notes in Computer Science, Vol. 8312, Springer, 2013.
Abstract
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.