Towards lightweight front-end for Isabelle/Isar
Mikhail Kazdagli, Andrei Lapets · 2011
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.