| Publication type: |
Article in Proceedings |
| Author: |
David Aspinall, Ewen Denney, Christoph Lüth |
| Title: |
A Tactic Language for Hiproofs |
| Book / Collection title: |
Mathematical Knowledge Management MKM 2008, Intelligent Computer Mathematics |
| Volume: |
5144 |
| Page(s): |
339 – 354 |
| Series: |
Lecture Notes in Artificial Intelligence |
| Year published: |
2008 |
| Publisher: |
Springer |
| Abstract: |
We introduce and study a tactic language,Hitac, for constructing hierarchical proofs, known as hiproofs.
The idea of hiproofs is to superimpose a labelled hierarchical
nesting on an ordinary proof tree. The labels and nesting are used to describe the organisation of the proof, typically relating to its construction process. This can be useful for understanding and navigating the proof. Tactics in our language construct hiproof structure together with an underlying proof tree.
We provide both a big-step and a small-step operational
semantics for evaluating tactic expressions. The big-step semantics captures the intended meaning, whereas the small-step semantics hints at possible implementations and provides a unified notion of proof state. We prove that these notions are equivalent and construct valid proofs.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/mkm08.pdf |
| Status: |
Reviewed |
| Last updated: |
07. 07. 2011 |
|
 |
