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
基金
日本学术振兴会;
关键词
Theorem proving - Model checking;
D O I
10.1007/978-3-642-54624-2_31
中图分类号
学科分类号
摘要
引用
收藏
页码:630 / 656
相关论文
共 50 条
  • [21] Theorem proving for a theory of shape graphs
    Zhang Y.
    Chen Y.-Y.
    Li Z.-P.
    Jisuanji Xuebao/Chinese Journal of Computers, 2016, 39 (12): : 2460 - 2480
  • [22] APPROACH TO THEOREM PROVING IN TYPE THEORY
    ANDREWS, PB
    COHEN, EL
    JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (03) : 477 - 478
  • [23] 1ST-ORDER THEOREM-PROVING USING CONDITIONAL REWRITE RULES
    ZHANG, H
    KAPUR, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1988, 310 : 1 - 20
  • [24] Translating timed I/O automata specifications for theorem proving in PVS
    Lim, HP
    Kaynar, D
    Lynch, N
    Mitra, S
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2005, 3829 : 17 - 31
  • [25] TOWARDS A PROOF THEORY OF PARAMETERIZED SPECIFICATIONS
    PADAWITZ, P
    LECTURE NOTES IN COMPUTER SCIENCE, 1984, 173 : 375 - 391
  • [26] Source-level proof reconstruction for interactive theorem proving
    Paulson, Lawrence C.
    Susanto, Kong Woei
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2007, 4732 : 232 - +
  • [27] Context-aware Generation of Proof Scripts for Theorem Proving
    Cheng, Chuanhu
    Xiong, Yan
    Huang, Wenchao
    Ma, Lu
    2020 6TH INTERNATIONAL CONFERENCE ON BIG DATA COMPUTING AND COMMUNICATIONS (BIGCOM 2020), 2020, : 81 - 85
  • [28] Learning Proof Path Selection Policies in Neural Theorem Proving
    Morris, Matthew
    Minervini, Pasquale
    Blunsom, Phil
    NEURAL-SYMBOLIC LEARNING AND REASONING, NESY 2022, 2022, : 64 - 87
  • [29] The use of proof planning for co-operative theorem proving
    Lowe, H
    Bundy, A
    McLean, D
    JOURNAL OF SYMBOLIC COMPUTATION, 1998, 25 (02) : 239 - 261
  • [30] Elementary Algebra Proof Exercises Using a Theorem Proving System
    Li, Bing
    Li, Lian
    PRACTICAL APPLICATIONS OF INTELLIGENT SYSTEMS, 2011, 124 : 275 - 280