Conference paper
Formal Methods Online: Sequent Calculus Verifier (SeCaV)
We present the Sequent Calculus Verifier (SeCaV) and discuss its advantages and disadvantages as a tool for teaching logic, automated reasoning and formal methods. SeCaV is a formalization in the proof assistant Isabelle/HOL of classical first-order logic with constants and functions. The syntax, the semantics and the inductive definition of the sequent calculus proof system along with the soundness and completeness proofs are verified in Isabelle/HOL.
SeCaV is accompanied by the SeCaV Unshortener, which is a browser application for developing sequent calculus proofs that are automatically translated into the corresponding Isabelle-embedded proofs. A compact format for the one-sided sequent calculus is used. The system provides feedback on proof rule applications.
Online help and examples are available. Hundreds of computer science students have used SeCaV for course exercises and exams. Reference: https://secav.compute.dtu.dk/
Language: | English |
---|---|
Year: | 2022 |
Proceedings: | Formal Methods Education Online: Tips, Tricks & Tools |
Types: | Conference paper |
ORCIDs: | From, Asta Halkjær , Jacobsen, Frederik Krogsdal and Villadsen, Jørgen |