Certification of proving termination of term rewriting by matrix interpretations

被引：0
作者：
Koprowski, Adam [1 ]
Zantema, Hans [1 ]
机构：
[1] Eindhoven Univ Technol, Dept Comp Sci, NL-5600 MB Eindhoven, Netherlands
来源：
SOFSEM 2008: THEORY AND PRACTICE OF COMPUTER SCIENCE | 2008年 / 4910卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We develop a Coq formalization of the matrix interpretation method, which is a recently developed, powerful approach to proving termination of term rewriting. Our formalization is a contribution to the CoLoR project and allows to automatically certify matrix interpretation proofs produced by tools for proving termination. Thanks to this development the combination of CoLoR and our tool, TPA, was the winner in 2007 in the new certified category of the annual Termination Competition.
引用
收藏
页码：328 / 339
页数：12
相关论文
共 14 条
  • [1] Termination of term rewriting using dependency pairs
    Arts, T
    Giesl, J
    [J]. THEORETICAL COMPUTER SCIENCE, 2000, 236 (1-2) : 133 - 178
  • [2] BLANQUI F, 2006, 8 WST
  • [3] CONTEJEAN E, CIME REWRITE TOOL
  • [4] Contejean E, 2007, LECT NOTES ARTIF INT, V4720, P148
  • [5] ENDRULLIS J, 2007, IN PRESS J AUTOMATED
  • [6] Endrullis J, 2006, LECT NOTES ARTIF INT, V4130, P574
  • [7] Giesl J, 2005, LECT NOTES COMPUT SC, V3452, P301
  • [8] Tyrolean termination tool: Techniques and features
    Hirokawa, Nao
    Middeldorp, Aart
    [J]. INFORMATION AND COMPUTATION, 2007, 205 (04) : 474 - 511
  • [9] KOPROWSKI A, 2007, 9 WST
  • [10] KOPROWSKI A, 2007, 0722 EINDH U TECHN
12