zbMATH — the first resource for mathematics

A web interface for Isabelle: the next generation. (English) Zbl 1390.68580
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 326-329 (2013).
Summary: We present Clide , a web interface for the interactive theorem prover Isabelle. Clide uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.
For the entire collection see [Zbl 1268.68008].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
PDF BibTeX Cite
Full Text: DOI