Querying Proofs (Work in Progress)
David Aspinall, Ewen Denney, Christoph Lueth · NASA Technical Reports Server (NASA) · 2011
We motivate and introduce the basis for a query language designed for inspecting electronic representations of proofs. We argue that there is much to learn from large proofs beyond their validity, and that a dedicated query language can provide a principled way of implementing a family of useful operations.