Projects per year
Abstract
We present an approach to mathematical assistants which uses readable, executable proof scripts as the central language for interaction. We examine an implementation that combines the Isar language, the Isabelle theorem prover and the IsaPlanner proof planner. We argue that this synergy provides a flexible environment for the exploration, certification, and presentation of mathematical proof.
Original language | English |
---|---|
Pages (from-to) | 505-532 |
Number of pages | 28 |
Journal | Journal of applied logic |
Volume | 4 |
Issue number | 4 |
DOIs | |
Publication status | Published - 2006 |
Keywords / Materials (for Non-textual outputs)
- Proof assistant
Fingerprint
Dive into the research topics of 'A proof-centric approach to mathematical assistants'. Together they form a unique fingerprint.Projects
- 1 Finished