Theorem proving based on proof scores for rewrite theory specifications of OTSs

被引：6
|
作者：
Ogata, Kazuhiro [1 ]
Futatsugi, Kokichi [1 ]
机构：
[1] School of Information Science, JAIST, Japan
来源：
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8373卷
基金：
日本学术振兴会;
关键词：
Theorem proving - Model checking;
D O I：
10.1007/978-3-642-54624-2_31
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：630 / 656
相关论文
共 50 条
  • [31] Learning Proof Transformations and Its Applications in Interactive Theorem Proving
    Zhang, Liao
    Blaauwbroek, Lasse
    Kaliszyk, Cezary
    Urban, Josef
    FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023, 2023, 14279 : 236 - 254
  • [32] AUTOMATIC THEOREM PROVING IN SET-THEORY
    PASTRE, D
    ARTIFICIAL INTELLIGENCE, 1978, 10 (01) : 1 - 27
  • [33] Automated theorem proving in quasigroup and loop theory
    Phillips, J. D.
    Stanovsky, David
    AI COMMUNICATIONS, 2010, 23 (2-3) : 267 - 283
  • [34] On the proof of the Π-theorem in dimension theory
    B. E. Pobedrya
    D. V. Georgievskii
    Russian Journal of Mathematical Physics, 2006, 13 : 431 - 437
  • [35] Conditional equational specifications of data types with partial operations for inductive theorem proving
    Kuhler, U
    Wirth, CP
    REWRITING TECHNIQUES AND APPLICATIONS, 1997, 1232 : 38 - 52
  • [36] Maude2Lean: Theorem proving for Maude specifications using Lean
    Rubio, Ruben
    Riesco, Adrian
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2025, 142
  • [37] Characteristics of Undergraduate Students' Mathematical Proof Construction on Proving Limit Theorem
    Netti, Syukma
    Herawati, Susi
    INTERNATIONAL CONFERENCE ON EDUCATIONAL SCIENCE AND TRAINING (FIRST ICEST), 2018, : 153 - 163
  • [38] User-oriented theorem proving with the ATINF graphic proof editor
    Caferra, R.
    Herment, M.
    Zabel, N.
    International Workshop on Fundamentals of Artificial Intelligence Research, 1991,
  • [39] Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies
    Mo, Guangshuai
    Xiong, Yan
    Huang, Wenchao
    Ma, Lu
    2020 6TH INTERNATIONAL CONFERENCE ON BIG DATA COMPUTING AND COMMUNICATIONS (BIGCOM 2020), 2020, : 71 - 75
  • [40] Rewrite-Based Decomposition of Signal Temporal Logic Specifications
    Leahy, Kevin
    Mann, Makai
    Vasile, Cristian-Ioan
    NASA FORMAL METHODS, NFM 2023, 2023, 13903 : 224 - 240
12345