A two-level approach towards lean proof-checking

被引：0
|
作者：
Barthe, G [1 ]
Ruys, M [1 ]
Barendregt, H [1 ]
机构：
[1] Univ Nijmegen, Fac Math & Informat, Nijmegen, Netherlands
来源：
TYPES FOR PROOFS AND PROGRAMS | 1996年 / 1158卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a simple and effective methodology for equational reasoning in proof checkers. The method is based on a two-level approach distinguishing between syntax and semantics of mathematical theories. The method is very general and can be carried out in any type system with inductive and oracle types. The potential of our two-level approach is illustrated by some examples developed in Lego.
引用
收藏
页码：16 / 35
页数：20
相关论文
共 50 条
  • [1] Proof-checking Euclid
    Beeson, Michael
    Narboux, Julien
    Wiedijk, Freek
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2019, 85 (2-4) : 213 - 257
  • [2] Proof-checking Euclid
    Michael Beeson
    Julien Narboux
    Freek Wiedijk
    [J]. Annals of Mathematics and Artificial Intelligence, 2019, 85 : 213 - 257
  • [3] Towards lean proof checking
    Barthe, G
    Elbers, H
    [J]. DESIGN AND IMPLEMENTATION OF SYMBOLIC COMPUTATION SYSTEMS, 1996, 1128 : 61 - 62
  • [4] Interactive and probabilistic proof-checking
    Trevisan, L
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 2000, 104 (1-3) : 325 - 342
  • [5] Proof-checking protocols using bisimulations
    Röckl, C
    Esparza, J
    [J]. CONCUR'99: CONCURRENCY THEORY, 1999, 1664 : 525 - 540
  • [6] Euclid after Computer Proof-Checking
    Beeson, Michael
    [J]. AMERICAN MATHEMATICAL MONTHLY, 2022, 129 (07): : 623 - 646
  • [7] A FORMALISM FOR PRIMITIVE LOGIC AND MECHANICAL PROOF-CHECKING
    ONO, K
    [J]. NAGOYA MATHEMATICAL JOURNAL, 1966, 26 (FEB) : 195 - &
  • [8] A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking
    Menezes, Bruno
    Martins, Ana Teresa
    Rocha, Thiago Alves
    [J]. FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2021, 2021, 13130 : 1 - 16
  • [9] READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
    Wenzel, Makarius
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (118): : 57 - 71
  • [10] THE PROOF-CHECKING COMPONENT FOR THE PLEATS PROGRAMMING SYSTEM ENABLING SPECIFICATION OF THEORIES
    CYBULKA, J
    BARTOSZEK, J
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 215 : 149 - 155
12345