Sciweavers

JAPLL
2006
104views more  JAPLL 2006»
13 years 5 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...
Lucas Dixon, Jacques D. Fleuriot
AISC
2008
Springer
13 years 7 months ago
Logic-Free Reasoning in Isabelle/Isar
Traditionally a rigorous mathematical document consists of a sequence of definition
Stefan Berghofer, Makarius Wenzel