Abstract
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/
| Original language | English |
|---|---|
| Publication date | 2022 |
| Number of pages | 1 |
| Publication status | Published - 2022 |
| Event | Formal Methods Education Online: Tips, Tricks & Tools - Technion, Haifa, Israel Duration: 31 Jul 2022 → 1 Aug 2022 https://www7.in.tum.de/~kretinsk/fomeo22.html |
Workshop
| Workshop | Formal Methods Education Online: Tips, Tricks & Tools |
|---|---|
| Location | Technion |
| Country/Territory | Israel |
| City | Haifa |
| Period | 31/07/2022 → 01/08/2022 |
| Internet address |