Edinburgh Research Explorer

A proof-centric approach to mathematical assistants

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Pages (from-to)505-532
Number of pages28
JournalJournal of applied logic
Issue number4
Publication statusPublished - 2006


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.

    Research areas

  • Proof assistant

Download statistics

No data available

ID: 22950327