Confluence Framework: Proving Confluence with CONFident

被引：5
作者：
Gutierrez, Raul [3 ]
Vitores, Miguel [1 ,2 ]
Lucas, Salvador [1 ,2 ]
机构：
[1] Univ Politecn Valencia, DSIC, Valencia, Spain
[2] Univ Politecn Valencia, VRAIN, Valencia, Spain
[3] Univ Politecn Madrid, DLSIIS, Madrid, Spain
来源：
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2022) | 2022年 / 13474卷
关键词：
Confluence; Program analysis; Rewriting; TERMINATION;
D O I：
10.1007/978-3-031-16767-6_2
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper describes CONFident, a tool which is able to automatically prove and disprove confluence of variants of rewrite systems: term rewriting systems, conditional term rewriting systems (using join, oriented, or semi-equational semantics), and context-sensitive term rewriting systems. We introduce a new proof framework to generate proof trees by combining different techniques for proving confluence (including modular decompositions, checking joinability of (conditional) critical pairs, transformations, etc.). We also use external tools for proving termination and operational termination (MU-TERM), or feasibility (infChecker) and deducibility (Prover9).
引用
收藏
页码：24 / 43
页数：20
相关论文
共 35 条
  • [1] Aoto T, 2009, LECT NOTES COMPUT SC, V5595, P93, DOI 10.1007/978-3-642-02348-4_7
  • [2] Baader F., 1998, TERM REWRITING ALL
  • [3] DERSHOWITZ N, 1988, LECT NOTES COMPUT SC, V308, P31
  • [4] Duran Francisco., 2004, PROC PEPM, P147, DOI DOI 10.1145/1014007.1014022
  • [5] Giesl J, 2005, LECT NOTES COMPUT SC, V3452, P301
  • [6] Mechanizing and improving dependency pairs
    Giesl, Juergen
    Thiemann, Rene
    Schneider-Kamp, Peter
    Falke, Stephan
    [J]. JOURNAL OF AUTOMATED REASONING, 2006, 37 (03) : 155 - 203
  • [7] Gmeiner K, 2013, 2 INT WORKSH CONFL I, P35
  • [8] Gmeiner K, 2012, Leibniz International Proceedings in Informatics (LIPIcs), V15, P193, DOI [10.4230/LIPIcs.RTA.2012.193, DOI 10.4230/LIPICS.RTA.2012.193]
  • [9] ORDER-SORTED ALGEBRA .1. EQUATIONAL DEDUCTION FOR MULTIPLE INHERITANCE, OVERLOADING, EXCEPTIONS AND PARTIAL OPERATIONS
    GOGUEN, JA
    MESEGUER, J
    [J]. THEORETICAL COMPUTER SCIENCE, 1992, 105 (02) : 217 - 273
  • [10] Gramlich B, 2006, LECT NOTES COMPUT SC, V4098, P66
1234