Sciweavers

Share
JAPLL
2006

A proof-centric approach to mathematical assistants

8 years 7 months ago
A proof-centric approach to mathematical assistants
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. Key words: proof planning, Isabelle, Isar, IsaPlanner, theorem proving, proof assistant
Lucas Dixon, Jacques D. Fleuriot
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAPLL
Authors Lucas Dixon, Jacques D. Fleuriot
Comments (0)
books