SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

• DOI: 10.4204/eptcs.357.4
• Publication Date: 2022-04-07T13:01:48Z
• Authors: Asta Halkjær From; Frederik Krogsdal...; Jørgen Villadsen
• Keywords: HOL; Sequent; Soundness; Expressive power; Proof assistant

We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into full syntax. leverage power of Isabelle/HOL as proof checker our derivations. The interactive features make system transparent. For instance, user can simply click on side condition to see its exact definition. Our formalized soundness completeness proofs pertain exactly exposed not just some model tool. Users also write their which provides lighter syntax, expand them later verification. have used both tools teaching.