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卷

关键词：

D O I：

16th Logical and Semantic Frameworks with Applications, LSFA 2021

中图分类号：

学科分类号：

摘要：

Differentiation (calculus) - Calculations - Formal logic - Theorem proving

引用

页码：38 / 55

共 50 条

[21] A Consistent Foundation for Isabelle/HOL
Kuncar, Ondrej
Popescu, Andrei
INTERACTIVE THEOREM PROVING, 2015, 9236 : 234 - 252
[22] A Consistent Foundation for Isabelle/HOL
Kuncar, Ondrej
Popescu, Andrei
JOURNAL OF AUTOMATED REASONING, 2019, 62 (04) : 531 - 555
[23] Owicki/Gries in Isabelle/HOL
Nipkow, T
Nieto, LP
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 1999, 1577 : 188 - 203
[24] Nominal Techniques in Isabelle/HOL
Christian Urban
Journal of Automated Reasoning, 2008, 40 : 327 - 356
[25] Idernpotent relations in Isabelle/HOL
Kammüller, F
Sanders, JW
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2004, 2005, 3407 : 310 - 324
[26] Formalisation of B in Isabelle/HOL
Chartier, P
B'98: RECENT ADVANCES IN THE DEVELOPMENT AND USE OF THE B METHOD, 1998, 1393 : 66 - 82
[27] Algebraic Numbers in Isabelle/HOL
Thiemann, Rene
Yamada, Akihisa
INTERACTIVE THEOREM PROVING (ITP 2016), 2016, 9807 : 391 - 408
[28] Hoare logics in Isabelle/HOL
Nipkow, T
PROOF AND SYSTEM-RELIABILITY, 2002, 62 : 341 - 367
[29] Liveness Reasoning with Isabelle/HOL
Wang, Jinshuang
Yang, Huabing
Zhang, Xingyuan
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 485 - 499
[30] Comprehending Isabelle/HOL's Consistency
Kuncar, Ondrej
Popescu, Andrei
PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 724 - 749