SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

被引：0
|
作者：
From, Asta Halkjær [1 ]
Jacobsen, Frederik Krogsdal [1 ]
Villadsen, Jørgen [1 ]
机构：
[1] DTU Compute, Department of Applied Mathematics and Computer Science, Technical University of Denmark, Denmark
来源：
Electronic Proceedings in Theoretical Computer Science, EPTCS | 2022年 / 357卷
关键词：
Compilation and indexing terms; Copyright 2024 Elsevier Inc;
D O I：
16th Logical and Semantic Frameworks with Applications, LSFA 2021
中图分类号：
学科分类号：
摘要：
Differentiation (calculus) - Calculations - Formal logic - Theorem proving
引用
收藏
页码：38 / 55
相关论文
共 50 条
  • [31] Fast Machine Words in Isabelle/HOL
    Lochbihler, Andreas
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 388 - 410
  • [32] A Modular Formalization of Superposition in Isabelle/HOL
    Desharnais, Martin
    Toth, Balazs
    Waldmann, Uwe
    Blanchette, Jasmin
    Tourret, Sophie
    Leibniz International Proceedings in Informatics, LIPIcs, 309
  • [33] A Denotational Semantics of Solidity in Isabelle/HOL
    Marmsoler, Diego
    Brucker, Achim D.
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021), 2021, 13085 : 403 - 422
  • [34] Automating Free Logic in Isabelle/HOL
    Benzmueller, Christoph
    Scott, Dana
    MATHEMATICAL SOFTWARE, ICMS 2016, 2016, 9725 : 43 - 50
  • [35] Verified Real Asymptotics in Isabelle/HOL
    Eberl, Manuel
    PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19), 2019, : 147 - 154
  • [36] Extracting a normalization algorithm in Isabelle/HOL
    Berghofer, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 50 - 65
  • [37] On the mechanization of real analysis in Isabelle/HOL
    Fleuriot, JD
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 145 - 161
  • [38] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
  • [39] A SEQUENT FORMULATION OF A LOGIC OF PREDICATES IN HOL
    CHOU, CT
    IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1993, 20 : 71 - 80
  • [40] Imperative functional programming with Isabelle/HOL
    Bulwahn, Lukas
    Krauss, Alexander
    Haftmann, Horian
    Erkoek, Levent
    Matthews, John
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 134 - +
12345