Towards lightweight front-end for Isabelle/Isar
Date
2011-09-10
DOI
Authors
Kazdagli, Mikhail
Lapets, Andrei
Version
OA Version
Citation
Kazdagli, Mikhail; Lapets, Andrei. "Towards Lightweight Front-end for Isabelle/Isar", Technical Report BUCS-TR-2011-021, Computer Science Department, Boston University, September 10, 2011. [Available from: http://hdl.handle.net/2144/11378]
Abstract
This work describes an attempt to assemble a lightweight prototype front-end for verifying propositional logic proofs that relies on the Isabelle/Isar proof authoring and verification system. This prototype serves as an opportunity to become familiar with some of Isabelle/Isar's verification capabilities and limitations, and provides a starting point for future work incorporating Isabelle/Isar as one of the underlying component tools in the Aartifact accessible integrated environment for formal modelling and verification.