Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

16

JAPLL
2006

favoriteEmaildiscussreport

104views more JAPLL 2006»

A proof-centric approach to mathematical assistants

13 years 4 months ago

A proof-centric approach to mathematical assistants

Download homepages.inf.ed.ac.uk

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

Real-time Traffic

Executable Proof | IsaPlanner Proof Planner | Isar Language | JAPLL 2006 |

claim paper

Related Content

» A Real Semantic Web for Mathematics Deserves a Real Semantics

» A Content Based Mathematical Search Engine Whelp

» The Conceptual and Architectural Design of a System Supporting Exploratory Learning of Mat...

» Towards intelligent motion inferencing in mathematical sketching

» Arguing on Issues with Mathematical Knowledge Items in a Semantic Wiki

» Computerizing Mathematical Text with MathLang

» A LargeScale Experiment in Executing Extracted Programs

» Blending Assessment and Instructional Assisting

» Assisted verification of elementary functions using Gappa

Post Info
More Details (n/a)

Added	13 Dec 2010
Updated	13 Dec 2010
Type	Journal
Year	2006
Where	JAPLL
Authors	Lucas Dixon, Jacques D. Fleuriot

Comments (0)