ConCon
Home Web-Interface References Experiments

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
[SW19]
Certified Ordered Completion
C. Sternagel, S. Winkler
doi: to appear