- Abstract:
-
We describe interactively tracing and exploring the application of proof planning techniques in IsaPlanner. The machinery is implemented by extending the language for expressing techniques with constructs that produce meaningful traces. We consider how the resulting tool can be used as an interface for theorem proving and as an aid to the development of techniques.
- Links To Paper
- Personal Copy
- Bibtex format
- @InProceedings{EDI-INF-RR-0892,
- author = {
Lucas Dixon
},
- title = {Interactive and Hierarchical Tracing of Techniques in IsaPlanner},
- book title = {Proceedings of the ETAPS-05 Workshop on User Interfaces for Theorem Provers (UITP-05)},
- publisher = {ENTCS},
- year = 2005,
- url = {http://homepages.inf.ed.ac.uk/ldixon/papers/uitp-05-traces.pdf},
- }
|
