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 条
  • [1] THE TERM REWRITING APPROACH TO AUTOMATED THEOREM-PROVING
    HSIANG, J
    KIRCHNER, H
    LESCANNE, P
    RUSINOWITCH, M
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1992, 14 (1-2): : 71 - 99
  • [2] REFUTATIONAL THEOREM-PROVING USING TERM-REWRITING SYSTEMS
    HSIANG, J
    [J]. ARTIFICIAL INTELLIGENCE, 1985, 25 (03) : 255 - 300
  • [3] PROVING INDUCTIVE THEOREMS BASED ON TERM REWRITING-SYSTEMS
    HOFBAUER, D
    KUTSCHE, RD
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1988, 343 : 180 - 190
  • [4] Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
    Kikuchi, Kentaro
    Aoto, Takahito
    Sasano, Isao
    [J]. PROCEEDINGS OF THE 21ST INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2019), 2019,
  • [5] 2 RESULTS IN TERM REWRITING THEOREM-PROVING
    HSIANG, J
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 202 : 301 - 324
  • [6] Proving Confluence of Term Rewriting Systems Automatically
    Aoto, Takahito
    Yoshida, Junichi
    Toyama, Yoshihito
    [J]. REWRITING TECHNIQUES AND APPLICATIONS, 2009, 5595 : 93 - 102
  • [7] PLATO: A tool to assist programming as term rewriting and theorem proving
    Sampaio, AJ
    Haeberer, AM
    Prates, CT
    Ururahy, CD
    Frias, MF
    Albuquerque, NC
    [J]. TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 797 - 798
  • [8] PROVING TERMINATION FOR TERM REWRITING-SYSTEMS
    WEIERMANN, A
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 419 - 428
  • [9] USE OF CONDITIONAL TERM REWRITING-SYSTEMS IN AUTOMATIC THEOREM-PROVING .1.
    VOROBYEV, SG
    [J]. SOVIET JOURNAL OF COMPUTER AND SYSTEMS SCIENCES, 1989, 27 (01): : 49 - 59
  • [10] Analogy in Inductive Theorem Proving
    Erica Melis
    Jon Whittle
    [J]. Journal of Automated Reasoning, 1999, 22 : 117 - 147