In the following we sum up some important references which are used in the proofs of ConCon and where most of the examples for our experiments come from.
Conditional Rewrite Rules
S. Kaplan
doi: 10.1016/0304-3975(84)90087-2
Conditional Rewrite Rules: Confluence and Termination
J. Bergstra, J. Klop
doi: 10.1016/0022-0000(86)90033-4
Confluence of Conditional Rewrite Systems
N. Dershowitz, M. Okada, G. Sivakumar
doi: 10.1007/3-540-19242-5_3
A Logical Analysis on Theory of Conditional Rewriting
M. Okada
doi: 10.1007/3-540-19242-5_14
Proof by Consistency in Conditional Equational Theories
E. Bevers, J. Lewi
doi: 10.1007/3-540-54317-1_91
Confluence of the Disjoint Union of Conditional Term Rewriting Systems
A. Middeldorp
doi: 10.1007/3-540-54317-1_99
Extended Term Rewriting Systems
J. Klop, R. de Vrijer
doi: 10.1007/3-540-54317-1_79
A Completion Procedure for Conditional Equationst
H. Ganzinger
doi: 10.1016/S0747-7171(08)80132-0
A Proof System for Conditional Algebraic Specifications
E. Kounalis, M. Rusinowitch
doi: 10.1007/3-540-54317-1_80
Sufficient Conditions for Modular Termination of Conditional Term Rewriting Systems
B. Gramlich
doi: 10.1007/3-540-56393-8_9
Denotational versus Declarative Semantics for Functional Programming
J. González Moreno, M. Hortalá González, M. Rodríguez Artalejo
doi: 10.1007/BFb0023763
Termination Proofs of Well-moded Logic Programs via Conditional Rewrite Systems
H. Ganzinger, U. Waldmann
doi: 10.1007/3-540-56393-8_34
Completeness of Combinations of Conditional Constructor Systems
A. Middeldorp
doi: 10.1007/3-540-56393-8_6
Modular Properties of Conditional Term Rewriting Systems
A. Middeldorp
doi: 10.1006/inco.1993.1027
On Conditional Rewrite Systems with Extra Variables and Deterministic Logic Programs
J. Avenhaus, C. Loría-Sáenz
doi: 10.1007/3-540-58216-9_40
On Termination and Confluence of Conditional Rewrite Systems
B. Gramlich
doi: 10.1007/3-540-60381-6_10
Church-Rosser Property and Unique Normal Form Property of Non-duplicating Term Rewriting Systems
Y. Toyama, M. Oyamaguchi
doi: 10.1007/3-540-60381-6_19
Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides
T. Suzuki, A. Middeldorp, T. Ida
doi: 10.1007/3-540-59200-8_56
On Deterministic Conditional Rewriting
M. Marchiori
Term Rewriting and All That
F. Baader, T. Nipkow
Termination of Term Rewriting using Dependency Pairs
T. Arts, J. Giesl
doi: 10.1016/S0304-3975(99)00207-8
Verification of Erlang Processes by Dependency Pairs
J. Giesl, T. Arts
doi: 10.1007/s002000100063
Termination of Logic Programs: Transformational Methods Revisited
E. Ohlebusch
doi: 10.1007/s002000100064
Advanced Topics in Term Rewriting
E. Ohlebusch
doi: 10.1007/978-1-4757-3661-8
Term Rewriting Systems
Transformational Approach to Inverse Computation in Term Rewriting
N. Nishida
Proving and Disproving Termination of Higher-Order Functions
J. Giesl, R. Thiemann, P. Schneider-Kamp
doi: 10.1007/11559306_12
From Conditional to Unconditional Rewriting
G. Roşu
doi: 10.1007/978-3-540-31959-7_13
Computationally Equivalent Elimination of Conditions
F. Şerbănuţă, G. Roşu
doi: 10.1007/11805618_3
Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems
F. Schernhammer, B. Gramlich
doi: 10.1016/j.jlap.2009.08.001
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
N. Nishida, M. Sakai, T. Sakabe
doi: 10.2168/LMCS-8(3:4)2012
Determinization of Conditional Term Rewriting Systems
M. Nagashima, M. Sakai, T. Sakabe
doi: 10.1016/j.tcs.2012.09.005
Proving Confluence of Conditional Term Rewriting Systems via Unravelings
K. Gmeiner, N. Nishida, B. Gramlich
In Proc. 2nd IWC, pages 35-39, 2013
On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs
M. Nakamura, K. Ogata, K. Futatsugi
Transformational Approaches for Conditional Term Rewrite Systems
K. Gmeiner
PhD Thesis
Formalizing Soundness and Completeness of Unravelings
S. Winkler, R. Thiemann
doi: 10.1007/978-3-319-24246-0_15
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
C. Sternagel, T. Sternagel
doi: 10.4230/LIPIcs.FSCD.2016.29
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
C. Sternagel, T. Sternagel
doi: 10.1007/978-3-319-63046-5_26
Certified Non-Confluence with ConCon 1.5
T. Sternagel, C. Sternagel
Reliable Confluence Analysis of Conditional Term Rewrite Systems
T. Sternagel
PhD Thesis
Certified Ordered Completion
C. Sternagel, S. Winkler
doi: to appear