Formal Methods Online: Sequent Calculus Verifier (SeCaV)

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

1 Downloads (Pure)


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:
Original languageEnglish
Publication date2022
Number of pages1
Publication statusPublished - 2022
EventFormal Methods Education Online: Tips, Tricks & Tools - Technion, Haifa, Israel
Duration: 31 Jul 20221 Aug 2022


WorkshopFormal Methods Education Online: Tips, Tricks & Tools
Internet address


Dive into the research topics of 'Formal Methods Online: Sequent Calculus Verifier (SeCaV)'. Together they form a unique fingerprint.

Cite this