A proof-centric approach to mathematical assistants Export

@article{citeulike:5921705, 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.}, author = {Dixon, L. and Fleuriot, J.}, citeulike-article-id = {5921705}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.jal.2005.10.007}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1570868305000728}, doi = {10.1016/j.jal.2005.10.007}, issn = {15708683}, journal = {Journal of Applied Logic}, keywords = {isabelle, proof-assistants, theorem-proving}, month = {December}, number = {4}, pages = {505--532}, posted-at = {2009-10-11 18:49:18}, priority = {2}, title = {A proof-centric approach to mathematical assistants}, url = {http://dx.doi.org/10.1016/j.jal.2005.10.007}, volume = {4}, year = {2006} }

TY - JOUR ID - citeulike:5921705 L3 - citeulike-article-id:5921705 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. IS - 4 JF - Journal of Applied Logic SN - 15708683 EP - 532 TI - A proof-centric approach to mathematical assistants VL - 4 SP - 505 KW - isabelle KW - proof-assistants KW - theorem-proving AU - Dixon, L AU - Fleuriot, J PY - 2006/12// UR - http://dx.doi.org/10.1016/j.jal.2005.10.007 ER -