TY - JOUR
T1 - A proof-centric approach to mathematical assistants
AU - Dixon, Lucas
AU - Fleuriot, Jacques
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
KW - Proof assistant
U2 - 10.1016/j.jal.2005.10.007
DO - 10.1016/j.jal.2005.10.007
M3 - Article
VL - 4
SP - 505
EP - 532
JO - Journal of applied logic
JF - Journal of applied logic
SN - 1570-8683
IS - 4
ER -