SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

15 Downloads (Pure)


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 the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condition to see its exact definition. Our formalized soundness and completeness proofs pertain exactly to the calculus as exposed to the user and not just to some model of our tool. Users can also write their derivations in the SeCaV Unshortener, which provides a lighter syntax, and expand them for later verification. We have used both tools in our teaching.
Original languageEnglish
Title of host publicationProceedings of 16th Logical and Semantic Frameworks with Applications
PublisherOpen Publishing Association
Publication date2022
Publication statusPublished - 2022
Event16th Sixteenth Logical and Semantic Frameworks with Applications - Online Event, Buenos Aires, Argentina
Duration: 23 Jul 202124 Jul 2021
Conference number: 16


Workshop16th Sixteenth Logical and Semantic Frameworks with Applications
LocationOnline Event
CityBuenos Aires
SeriesElectronic Proceedings in Theoretical Computer Science, EPTCS


Dive into the research topics of 'SeCaV: A Sequent Calculus Verifier in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this