Automated inductive theorem proving using transformations of term rewriting systems

被引：0
|
作者：
Sato, Koichi [1 ]
Kikuchi, Kentaro [1 ]
Aoto, Takahito [1 ]
Toyama, Yoshihito [1 ]
机构：
[1] Research Institute of Electrical Communication, Tohoku University, Japan
来源：
Computer Software | 2015年 / 32卷 / 01期
关键词：
Automated theorem proving - Automated verification - Functional programs - Inductive Theorem Proving - Program transformation techniques - Recursive programs - Tail recursive - Term rewriting systems;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：179 / 193
相关论文
共 50 条
  • [21] Automated theorem proving
    Plaisted, David A.
    WILEY INTERDISCIPLINARY REVIEWS-COGNITIVE SCIENCE, 2014, 5 (02) : 115 - 128
  • [22] Proving Termination by Dependency Pairs and Inductive Theorem Proving
    Fuhs, Carsten
    Giesl, Juergen
    Parting, Michael
    Schneider-Kamp, Peter
    Swiderski, Stephan
    JOURNAL OF AUTOMATED REASONING, 2011, 47 (02) : 133 - 160
  • [23] Reasoning support for CASL with automated theorem proving systems
    Luettich, Klaus
    Mossakowski, Till
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES, 2007, 4409 : 74 - +
  • [24] Evaluating general purpose automated theorem proving systems
    Sutcliffe, G
    Suttner, C
    ARTIFICIAL INTELLIGENCE, 2001, 131 (1-2) : 39 - 54
  • [25] Combining Clifford algebraic computing and term-rewriting for geometric theorem proving
    Fevre, Stephane
    Wang, Dongming
    Fundamenta Informaticae, 1999, 39 (1-2): : 85 - 104
  • [26] Inductive Theorem Proving for Design Specifications
    J Symb Comput, 1 (41):
  • [27] Inductive theorem proving for design specifications
    Padawitz, P
    JOURNAL OF SYMBOLIC COMPUTATION, 1996, 21 (01) : 41 - 99
  • [28] Machine Learning for Inductive Theorem Proving
    Jiang, Yaqing
    Papapanagiotou, Petros
    Fleuriot, Jacques
    ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION (AISC 2018), 2018, 11110 : 87 - 103
  • [29] A PATH ORDERING FOR PROVING TERMINATION OF TERM REWRITING-SYSTEMS
    KAPUR, D
    NARENDRAN, P
    SIVAKUMAR, G
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 185 : 173 - 187
  • [30] Mechanizing weak termination proving of term rewriting systems by induction
    Feng, S
    Cao, S
    Liu, SX
    COMPUTER SCIENCE AND TECHNOLOGY IN NEW CENTURY, 2001, : 15 - 19
12345