Formalizing rewriting in the ACL2 theorem prover

被引：0
|
作者：
Ruiz-Reina, JL [1 ]
Alonso, JA [1 ]
Hidalgo, MJ [1 ]
Martín-Mateos, FJ [1 ]
机构：
[1] Univ Sevilla, Dept Ciencias Computac & Inteligencia Artificial, Fac Informat & Estadist, E-41012 Seville, Spain
来源：
ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION | 2001年 / 1930卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation systems, since the notion of rewriting or simplification is ubiquitous in such systems. We concentrate here on formalization and representation aspects of abstract reduction and term rewriting systems, using the first-order, quantifier-free ACL2 logic based on Common Lisp.
引用
收藏
页码：92 / 106
页数：15
相关论文
共 50 条
  • [1] Milestones from the Pure Lisp theorem prover to ACL2
    Moore, J. Strother
    [J]. FORMAL ASPECTS OF COMPUTING, 2019, 31 (06) : 699 - 732
  • [2] Proceedings - 17th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2022
    [J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 359
  • [3] Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
    Mehta, Mihir Parang
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 18 - 29
  • [4] Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover
    Smith, Eric
    Coglio, Alessandro
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 183 - 201
  • [5] Verification of Year 2000 conversion rules using the ACL2 theorem prover
    Kaufmann M.
    [J]. International Journal on Software Tools for Technology Transfer, 2000, 3 (1) : 13 - 19
  • [6] Rewriting with equivalence relations in ACL2
    Brock, Bishop
    Kaufmann, Matt
    Moore, J. Strother
    [J]. JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 293 - 306
  • [7] Rewriting with Equivalence Relations in ACL2
    Bishop Brock
    Matt Kaufmann
    J Strother Moore
    [J]. Journal of Automated Reasoning, 2008, 40 : 293 - 306
  • [8] The Fundamental Theorem of Algebra in ACL2
    Gamboa, Ruben
    Cowles, John
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 98 - 110
  • [9] Formal Proofs About Rewriting Using ACL2
    José-Luis Ruiz-Reina
    José-Antonio Alonso
    María-José Hidalgo
    Francisco-Jesús Martín-Mateos
    [J]. Annals of Mathematics and Artificial Intelligence, 2002, 36 : 239 - 262
  • [10] Formal proofs about rewriting using ACL2
    Ruiz-Reina, JL
    Alonso, JA
    Hidalgo, MJ
    Martín-Mateos, FJ
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2002, 36 (03) : 239 - 262
12345