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 条
  • [1] Transforming SAT into Termination of Rewriting
    Zankl, Harald
    Sternagel, Christian
    Middeldorp, Aart
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 246 : 199 - 214
  • [2] A Pearl on SAT Solving in Prolog
    Howe, Jacob M.
    King, Andy
    FUNCTIONAL AND LOGIC PROGRAMMING, PROCEEDINGS, 2010, 6009 : 165 - +
  • [3] SAT solving for termination analysis with polynomial interpretations
    Fuhs, Carsten
    Giesl, Juergen
    Middeldorp, Aart
    Schneider-Kamp, Peter
    Thiemann, Rene
    Zankl, Harald
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2007, PROCEEDINGS, 2007, 4501 : 340 - +
  • [4] A pearl on SAT and SMT solving in Prolog
    Howe, Jacob M.
    King, Andy
    THEORETICAL COMPUTER SCIENCE, 2012, 435 : 43 - 55
  • [5] Termination of term rewriting using dependency pairs
    Arts, T
    Giesl, J
    THEORETICAL COMPUTER SCIENCE, 2000, 236 (1-2) : 133 - 178
  • [6] Proving termination using recursive path orders and SAT solving
    Schneider-Kamp, Peter
    Thiemann, Ren
    Annov, Elena
    Codish, Michael
    Giesl, Juergen
    FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 267 - +
  • [7] The Termination Hierarchy for Term Rewriting
    H. Zantema
    Applicable Algebra in Engineering, Communication and Computing, 2001, 12 : 3 - 19
  • [8] Total termination of term rewriting
    Ferreira, MCF
    Zantema, H
    APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 1996, 7 (02) : 133 - 162
  • [9] Automated termination analysis for logic programs by term rewriting
    Schneider-Kamp, Peter
    Giesl, Juergen
    Serebrenik, Alexander
    Thiemann, Rene
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2007, 4407 : 177 - +
  • [10] The termination hierarchy for term rewriting
    Zantema, H
    APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 2001, 12 (1-2) : 3 - 19
12345