References

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.
[K84]
Conditional Rewrite Rules
S. Kaplan
doi: 10.1016/0304-3975(84)90087-2
[BK86]
Conditional Rewrite Rules: Confluence and Termination
J. Bergstra, J. Klop
doi: 10.1016/0022-0000(86)90033-4
[DOS87]
Confluence of Conditional Rewrite Systems
N. Dershowitz, M. Okada, G. Sivakumar
doi: 10.1007/3-540-19242-5_3
[O88a]
A Logical Analysis on Theory of Conditional Rewriting
M. Okada
doi: 10.1007/3-540-19242-5_14
[BL90]
Proof by Consistency in Conditional Equational Theories
E. Bevers, J. Lewi
doi: 10.1007/3-540-54317-1_91
[M90]
Confluence of the Disjoint Union of Conditional Term Rewriting Systems
A. Middeldorp
doi: 10.1007/3-540-54317-1_99
[KV90]
Extended Term Rewriting Systems
J. Klop, R. de Vrijer
doi: 10.1007/3-540-54317-1_79
[G91]
A Completion Procedure for Conditional Equationst
H. Ganzinger
doi: 10.1016/S0747-7171(08)80132-0
[KR91]
A Proof System for Conditional Algebraic Specifications
E. Kounalis, M. Rusinowitch
doi: 10.1007/3-540-54317-1_80
[G92]
Sufficient Conditions for Modular Termination of Conditional Term Rewriting Systems
B. Gramlich
doi: 10.1007/3-540-56393-8_9
[GMHGRA92]
Denotational versus Declarative Semantics for Functional Programming
J. González Moreno, M. Hortalá González, M. Rodríguez Artalejo
doi: 10.1007/BFb0023763
[GW92]
Termination Proofs of Well-moded Logic Programs via Conditional Rewrite Systems
H. Ganzinger, U. Waldmann
doi: 10.1007/3-540-56393-8_34
[M92]
Completeness of Combinations of Conditional Constructor Systems
A. Middeldorp
doi: 10.1007/3-540-56393-8_6
[M93]
Modular Properties of Conditional Term Rewriting Systems
A. Middeldorp
doi: 10.1006/inco.1993.1027
[ALS94]
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
[G94]
On Termination and Confluence of Conditional Rewrite Systems
B. Gramlich
doi: 10.1007/3-540-60381-6_10
[TO94]
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
[SMI95]
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
[M97]
On Deterministic Conditional Rewriting
M. Marchiori
link: http://www.w3.org/People/Massimo/papers/MIT-LCS-TM-405.pdf
[BN98]
Term Rewriting and All That
F. Baader, T. Nipkow
link: http://www21.in.tum.de/~nipkow/TRaAT/
[AG00]
Termination of Term Rewriting using Dependency Pairs
T. Arts, J. Giesl
doi: 10.1016/S0304-3975(99)00207-8
[GA01]
Verification of Erlang Processes by Dependency Pairs
J. Giesl, T. Arts
doi: 10.1007/s002000100063
[O01b]
Termination of Logic Programs: Transformational Methods Revisited
E. Ohlebusch
doi: 10.1007/s002000100064
[O02]
Advanced Topics in Term Rewriting
E. Ohlebusch
doi: 10.1007/978-1-4757-3661-8
[TeReSe]
Term Rewriting Systems
Terese
link: http://www.cs.vu.nl/~terese/
[N04]
Transformational Approach to Inverse Computation in Term Rewriting
N. Nishida
link: http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf
[GTSK05]
Proving and Disproving Termination of Higher-Order Functions
J. Giesl, R. Thiemann, P. Schneider-Kamp
doi: 10.1007/11559306_12
[R05]
From Conditional to Unconditional Rewriting
G. Roşu
doi: 10.1007/978-3-540-31959-7_13
[SR06]
Computationally Equivalent Elimination of Conditions
F. Şerbănuţă, G. Roşu
doi: 10.1007/11805618_3
[SG10]
Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems
F. Schernhammer, B. Gramlich
doi: 10.1016/j.jlap.2009.08.001
[NSS12]
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
[NSS12b]
Determinization of Conditional Term Rewriting Systems
M. Nagashima, M. Sakai, T. Sakabe
doi: 10.1016/j.tcs.2012.09.005
[GNG13]
Proving Confluence of Conditional Term Rewriting Systems via Unravelings
K. Gmeiner, N. Nishida, B. Gramlich
In Proc. 2nd IWC, pages 35-39, 2013
[NOF13]
On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs
M. Nakamura, K. Ogata, K. Futatsugi
link: http://www.iaeng.org/IJCS/issues_v40/issue_2/IJCS_40_2_08.pdf
[G14]
Transformational Approaches for Conditional Term Rewrite Systems
K. Gmeiner
PhD Thesis
[WT15]
Formalizing Soundness and Completeness of Unravelings
S. Winkler, R. Thiemann
doi: 10.1007/978-3-319-24246-0_15
[SS16]
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
C. Sternagel, T. Sternagel
doi: 10.4230/LIPIcs.FSCD.2016.29
[SS17]
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
C. Sternagel, T. Sternagel
doi: 10.1007/978-3-319-63046-5_26
[SS17b]
Certified Non-Confluence with ConCon 1.5
T. Sternagel, C. Sternagel
link: http://cl-informatik.uibk.ac.at/events/iwc-2017/pdf/iwc2017.pdf
[T17]
Reliable Confluence Analysis of Conditional Term Rewrite Systems
T. Sternagel
PhD Thesis