Static Termination Analysis for Prolog Using Term Rewriting and SAT Solving

被引：0
|
作者：
Schneider-Kamp, Peter
机构：
来源：
KUNSTLICHE INTELLIGENZ | 2010年 / 24卷 / 01期
关键词：
Logic Programming; Modular Framework; Program Transformation; Prolog Program; Ranking Function;
D O I：
10.1007/s13218-010-0015-5
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The dissertation "Static Termination Analysis for Prolog using Term Rewriting and SAT Solving" (SchneiderKamp in Dissertation, RWTH Aachen University, 2008) presents a fresh approach to automated termination analysis of Prolog programs. This approach is based on the following three main concepts: the use of program transformations to obtain simpler termination problems, a framework for modular termination analysis, and the encoding of search problems into satisfiability of propositional logic (SAT) for efficient generation of ranking functions.
引用
收藏
页码：79 / 81
页数：3
相关论文
共 50 条
  • [41] A STATIC ANALYSIS OF PROLOG PROGRAMS
    MATSUMOTO, H
    SIGPLAN NOTICES, 1985, 20 (10): : 48 - 59
  • [42] Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis
    Johannes Waldmann
    Hans Zantema
    Journal of Automated Reasoning, 2008, 40 : 195 - 220
  • [43] Size-change termination for term rewriting
    Thiemann, R
    Giesl, J
    REWRITING TECNIQUES AND APPLICATIONS, PROCEEDINGS, 2003, 2706 : 264 - 278
  • [44] Matrix interpretations for proving termination of term rewriting
    Endrullis, Jorg
    Waldmann, Johannes
    Zantema, Hans
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 574 - 588
  • [45] TERMINATION OF LINEAR BOUNDED TERM REWRITING SYSTEMS
    Durand, Irene
    Senizergues, Geraud
    Sylvestre, Marc
    PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10), 2010, 6 : 341 - 356
  • [46] Detecting non-termination of term rewriting systems using an unfolding operator
    Payet, Etienne
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2007, 4407 : 194 - 209
  • [47] Reachability Analysis for Termination and Confluence of Rewriting
    Sternagel, Christian
    Yamada, Akihisa
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 : 262 - 278
  • [48] Automated Termination Proofs for Logic Programs by Term Rewriting
    Schneider-Kamp, Peter
    Giesl, Juergen
    Serebrenik, Alexander
    Thiemann, Rene
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 11 (01)
  • [49] A LOCAL TERMINATION PROPERTY FOR TERM REWRITING-SYSTEMS
    LATCH, DM
    SIGAL, R
    LECTURE NOTES IN COMPUTER SCIENCE, 1989, 355 : 222 - 233
  • [50] Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
    Neurauter, Friedrich
    Middeldorp, Aart
    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11), 2011, 10 : 251 - 266
12345