论文标题
SECAV：Isabelle/HOL中的序列验证器
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
论文作者
论文摘要
我们描述了SECAV，这是Isabelle/Hol中一阶逻辑的序列验证器，以及Secav Unshortener，它是一种在线工具，可将简洁的推导扩展到完整的SECAV语法中。我们利用Isabelle/Hol作为SECAV推导的证明检查器的力量。 Isabelle/HOL的交互作用使我们的系统透明。例如，用户只需单击侧面条件即可查看其确切的定义。我们正式的声音性和完整性证明完全涉及与用户暴露的微积分有关的，而不仅仅是我们工具的某些型号。用户还可以在SECAV UnshortEner中编写其派生，该secav unshortener提供了更轻的语法，并将其扩展以供以后验证。我们在教学中使用了这两个工具。
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.
