SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

Asta Halkjær From; Frederik Krogsdal Jacobsen; Jørgen Villadsen

doi:10.4204/EPTCS.357.4

SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

51 Downloads (Pure)

Abstract

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 language	English
Title of host publication	Proceedings of 16^th Logical and Semantic Frameworks with Applications
Volume	357
Publisher	Open Publishing Association
Publication date	2022
Pages	38-55
DOIs	https://doi.org/10.4204/EPTCS.357.4
Publication status	Published - 2022
Event	16^th Sixteenth Logical and Semantic Frameworks with Applications - Online Event, Buenos Aires, Argentina Duration: 23 Jul 2021 → 24 Jul 2021 Conference number: 16

Workshop

Workshop	16^th Sixteenth Logical and Semantic Frameworks with Applications
Number	16
Location	Online Event
Country/Territory	Argentina
City	Buenos Aires
Period	23/07/2021 → 24/07/2021

Series	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	357
ISSN	2075-2180

Access to Document

10.4204/EPTCS.357.4

FulltextFinal published version, 386 KB

OpenUrl availability

Full text

Cite this

@inproceedings{ea97cfdc7392433cabb42357474e39ca,

title = "SeCaV: A Sequent Calculus Verifier in Isabelle/HOL",

abstract = "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.",

author = "From, {Asta Halkj{\ae}r} and Jacobsen, {Frederik Krogsdal} and J{\o}rgen Villadsen",

year = "2022",

doi = "10.4204/EPTCS.357.4",

language = "English",

volume = "357",

series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

publisher = "Open Publishing Association",

pages = "38--55",

booktitle = "Proceedings of 16th Logical and Semantic Frameworks with Applications",

note = "16<sup>th</sup> Sixteenth Logical and Semantic Frameworks with Applications, LSFA 2021 ; Conference date: 23-07-2021 Through 24-07-2021",

}

From, AH, Jacobsen, FK & Villadsen, J 2022, SeCaV: A Sequent Calculus Verifier in Isabelle/HOL. in Proceedings of 16^th Logical and Semantic Frameworks with Applications. vol. 357, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 357, pp. 38-55, 16^th Sixteenth Logical and Semantic Frameworks with Applications, Buenos Aires, Argentina, 23/07/2021. https://doi.org/10.4204/EPTCS.357.4

SeCaV: A Sequent Calculus Verifier in Isabelle/HOL. / From, Asta Halkjær; Jacobsen, Frederik Krogsdal ; Villadsen, Jørgen.
Proceedings of 16^th Logical and Semantic Frameworks with Applications. Vol. 357 Open Publishing Association, 2022. p. 38-55 (Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 357).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

AU - From, Asta Halkjær

AU - Jacobsen, Frederik Krogsdal

AU - Villadsen, Jørgen

N1 - Conference code: 16

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.357.4

DO - 10.4204/EPTCS.357.4

M3 - Article in proceedings

VL - 357

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 38

EP - 55

BT - Proceedings of 16th Logical and Semantic Frameworks with Applications

PB - Open Publishing Association

T2 - 16<sup>th</sup> Sixteenth Logical and Semantic Frameworks with Applications

Y2 - 23 July 2021 through 24 July 2021

ER -

SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

Abstract

Workshop

Access to Document

OpenUrl availability

Fingerprint

Cite this