A Semantic Basis for Proof Queries and Transformations

David Aspinall, Ewen Denney, Christoph Lüth

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We add updates to the query language PrQL, designed for inspecting machine representations of proofs. PrQL natively supports hiproofs that express proof structure using hierarchically nested labelled trees, which we claim is a natural way of taming the complexity of huge proofs. Query-driven updates allow us to change this structure, in particular, to transform proofs produced by interactive theorem provers into forms that are easier for humans to understand, or that could be consumed by other tools. In this paper we motivate and define basic update operations, using an 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 or manipulate the hierarchy to group and ungroup nodes. We show that these basic operations are well-behaved and hence can form a sound core for a hierarchical transformation language. Our study here is firmly in language design and semantics; implementation strategies and study of sub-languages of our query language with good complexity will come later.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
EditorsKen McMillan, Aart Middeldorp, Andrei Voronkov
PublisherSpringer Berlin Heidelberg
Number of pages18
ISBN (Electronic)978-3-642-45221-5
ISBN (Print)978-3-642-45220-8
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'A Semantic Basis for Proof Queries and Transformations'. Together they form a unique fingerprint.

Cite this