Automating Equational Proofs in Dirac Notation

被引：0

作者：

Xu, Yingte ^{[1
]}

Barthe, Gilles ^{[2
]}

Zhou, Li ^{[3
]}

机构：

[1] Germany and Institute of Software, MPI-SP, Chinese Academy of Sciences, China

[2] Germany and IMDEA Software Institute, MPI-SP, Spain

[3] Institute of Software, Chinese Academy of Sciences, China

来源：

Proceedings of the ACM on Programming Languages | 2025年 / 9卷

关键词：

This research was supported by the National Key R&D Program of China under Grant No. 2023YFA1009403 and by Deutsche Forschungsgemeinschaft (DFG; German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments - EXC 2092 CASA - 390781972;

D O I：

10.1145/3704878

中图分类号：

学科分类号：

摘要：

引用

共 50 条

[1] Groupoid of equational proofs
Kinoshita, Yoshiki
Takahasi, Koichi
Denshi Gijutsu Sogo Kenkyusho Iho/Bulletin of the Electrotechnical Laboratory, 1996, 60 (11): : 1 - 8
[2] Automating Proofs
Edwards, Chris
COMMUNICATIONS OF THE ACM, 2016, 59 (04) : 13 - 15
[3] Relational algebra and equational proofs
Fundam Inf, 1 (101):
[4] Automating Soundness Proofs
van Weerdenburg, Muck
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 229 (04) : 107 - 118
[5] Certifying and synthesizing membership equational proofs
Rosu, G
Eker, S
Lincoln, P
Meseguer, J
FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 359 - 380
[6] FOUNDATIONS OF EQUATIONAL DEDUCTION - A CATEGORICAL TREATMENT OF EQUATIONAL PROOFS AND UNIFICATION ALGORITHMS
RYDEHEARD, DE
STELL, JG
LECTURE NOTES IN COMPUTER SCIENCE, 1987, 283 : 114 - 139
[7] EQUATIONAL PROOFS OF JACOBSON’S THEOREM
Brandenburg, Martin
arXiv, 2023,
[8] PROOFS BY INDUCTION IN EQUATIONAL THEORIES WITH CONSTRUCTORS
HUET, G
HULLOT, JM
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (02) : 239 - 266
[9] THE EQUATIONAL PART OF PROOFS BY STRUCTURAL INDUCTION
LYSNE, O
BIT, 1993, 33 (04): : 596 - 618
[10] Automating the search for elegant proofs
Wos, L
JOURNAL OF AUTOMATED REASONING, 1998, 21 (02) : 135 - 175

← 1 2 3 4 5 →