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
中图分类号：
学科分类号：
摘要：
77
引用
收藏
相关论文
共 50 条
  • [21] Discovery of equational replacement proofs using the congruence closure
    Brena, R
    PROCEEDINGS ISAI/IFIS 1996 - MEXICO - USA COLLABORATION IN INTELLIGENT SYSTEMS TECHNOLOGIES, 1996, : 356 - 361
  • [22] Automating Change of Representation for Proofs in Discrete Mathematics
    Raggi, Daniel
    Bundy, Alan
    Grov, Gudmund
    Pease, Alison
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 227 - 242
  • [23] Investigating Student Difficulties with Dirac Notation
    Singh, Chandralekha
    Marshman, Emily
    2013 PHYSICS EDUCATION RESEARCH CONFERENCE, 2013, : 345 - 348
  • [24] LightDP: Towards automating differential privacy proofs
    Zhang D.
    Kifer D.
    2017, Association for Computing Machinery (52): : 888 - 901
  • [25] AUTOMATING MOST PARTS OF HARDWARE PROOFS IN HOL
    SCHNEIDER, K
    KUMAR, R
    KROPF, T
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 365 - 375
  • [26] LightDP: Towards Automating Differential Privacy Proofs
    Zhang, Danfeng
    Kifer, Daniel
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 888 - 901
  • [27] Students' metarepresentational competence with matrix notation and Dirac notation in quantum mechanics
    Wawro, Megan
    Watson, Kevin
    Christensen, Warren
    PHYSICAL REVIEW PHYSICS EDUCATION RESEARCH, 2020, 16 (02):
  • [28] Automating Geometric Proofs of Collision Avoidance with Active Corners
    Kheterpal, Nishant
    Tang, Elanor
    Jeannin, Jean-Baptiste
    2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 359 - 368
  • [29] Nuprl as logical framework for automating proofs in category theory
    Kreitz, Christoph
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012, 7230 LNCS : 124 - 148
  • [30] Improving QED-Tutrix by Automating the Generation of Proofs
    Font, Ludovic
    Richard, Philippe R.
    Gagnon, Michel
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (267): : 38 - 58
12345