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
    JOURNAL OF LOGIC PROGRAMMING, 1992, 14 (1-2): : 71 - 99
  • [2] REFUTATIONAL THEOREM-PROVING USING TERM-REWRITING SYSTEMS
    HSIANG, J
    ARTIFICIAL INTELLIGENCE, 1985, 25 (03) : 255 - 300
  • [3] PROVING INDUCTIVE THEOREMS BASED ON TERM REWRITING-SYSTEMS
    HOFBAUER, D
    KUTSCHE, RD
    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
    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
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 202 : 301 - 324
  • [6] Proving Confluence of Term Rewriting Systems Automatically
    Aoto, Takahito
    Yoshida, Junichi
    Toyama, Yoshihito
    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
    TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 797 - 798
  • [8] PROVING TERMINATION FOR TERM REWRITING-SYSTEMS
    WEIERMANN, A
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 419 - 428
  • [9] USE OF CONDITIONAL TERM REWRITING-SYSTEMS IN AUTOMATIC THEOREM-PROVING .1.
    VOROBYEV, SG
    SOVIET JOURNAL OF COMPUTER AND SYSTEMS SCIENCES, 1989, 27 (01): : 49 - 59
  • [10] Analogy in Inductive Theorem Proving
    Erica Melis
    Jon Whittle
    Journal of Automated Reasoning, 1999, 22 : 117 - 147
12345