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 条
  • [41] Differential Dynamic Logics Automated Theorem Proving for Hybrid Systems
    Platzer, Andre
    KUNSTLICHE INTELLIGENZ, 2010, 24 (01): : 75 - 77
  • [42] Proving Termination of Integer Term Rewriting
    Fuhs, Carsten
    Giesl, Juergen
    Pluecker, Martin
    Schneider-Kamp, Peter
    Falke, Stephan
    REWRITING TECHNIQUES AND APPLICATIONS, 2009, 5595 : 32 - +
  • [43] Checking Sufficient Completeness by Inductive Theorem Proving
    Meseguer, Jose
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2022, 2022, 13252 : 171 - 190
  • [44] Inductive theorem proving in hierarchical conditional specifications
    Avenhaus, J
    Madlener, K
    MODELS, ALGEBRAS, AND PROOFS, 1999, 203 : 337 - 371
  • [45] Inductive theorem proving based on tree grammars
    Eberhard, Sebastian
    Hetzl, Stefan
    ANNALS OF PURE AND APPLIED LOGIC, 2015, 166 (06) : 665 - 700
  • [46] Characterizing and proving operational termination of deterministic conditional term rewriting systems
    Schernhammer, Felix
    Gramlich, Bernhard
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2010, 79 (07): : 659 - 688
  • [47] Matrix-based inductive theorem proving
    Kreitz, C
    Pientka, B
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2000, 1847 : 294 - 308
  • [48] Connection-driven inductive theorem proving
    Kreitz C.
    Pientka B.
    Studia Logica, 2001, 69 (2) : 293 - 326
  • [49] Dependency pairs for proving termination properties of conditional term rewriting systems
    Lucas, Salvador
    Meseguer, Jose
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2017, 86 (01) : 236 - 268
  • [50] Inductive inference of term rewriting systems from positive data
    Rao, MRKK
    ALGORITHMIC LEARNING THEORY, PROCEEDINGS, 2004, 3244 : 69 - 82