A proof-centric approach to mathematical assistants

Lucas Dixon, Jacques Fleuriot

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)505-532
Number of pages28
JournalJournal of applied logic
Volume4
Issue number4
DOIs
Publication statusPublished - 2006

Keywords

  • Proof assistant

Fingerprint

Dive into the research topics of 'A proof-centric approach to mathematical assistants'. Together they form a unique fingerprint.

Cite this