VSL 2014: VIENNA SUMMER OF LOGIC 2014
IWC ON SUNDAY, JULY 13TH, 2014

View: session overviewtalk overviewside by side with other conferences

09:25-10:15 Session 25: Opening and invited talk
Location: FH, Seminarraum 303
09:25
On the Formalization of Lambda-Calculus Confluence and Residuals
10:15-10:45Coffee Break
10:45-11:45 Session 26J: Regular talks
Location: FH, Seminarraum 303
10:45
Certification of Confluence Proofs using CeTA

ABSTRACT. CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By now, CeTA can also be used for certifying confluence and non-confluence proofs. In this system description, we give a short overview on what kind of proofs are supported, and what information has to be given in the certificates. As we will see, only a small amount of information is required and so we hope that CSI will not stay the only confluence tool which can produce certificates.

11:15
Confluence and Critical-Pair-Closing Systems
SPEAKER: Nao Hirokawa

ABSTRACT. In this note we introduce critical-pair-closing systems which are aimed at analyzing confluence of term rewriting systems. Based on the notion two new confluence criteria are presented. One is a generalization of weak orthogonality based on relative termination, and another is a partial solution to the RTA Open Problem #13.

12:00-13:00 Session 29A: Regular talks
Location: FH, Seminarraum 303
12:00
Critical Pairs in Network Rewriting

ABSTRACT. This extended abstract breifly introduces rewriting of networks (directed acyclic graphs with the extra structure needed to serve as expressions for PROducts and Permutations categories) and describes the critical pairs aspects of this theory.

12:30
On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation
SPEAKER: Naoki Nishida

ABSTRACT. This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu  transformation, which has informally been proposed in the literature. 

13:00-14:30Lunch Break
14:30-15:30 Session 31D: Joint IWC / TermGraph Invited Talk (joint with TermGraph)
Location: FH, Seminarraum 325/2
14:30
An Introduction to Higher-Dimensional Rewriting Theory
SPEAKER: Samuel Mimram
15:30-16:00 Session 33B: Regular talk
Location: FH, Seminarraum 303
15:30
Confluence of linear rewriting and homology of algebras

ABSTRACT. We introduce the notion of higher dimensional linear rewriting system for presentations of algebras generalizing the notion of noncommutative Gröbner bases. We show how to use this notion to compute homological invariants of associative algebras, related to confluence properties of presentations of these algebras. Our method constitutes a new application of confluence in algebra.

16:00-16:30Coffee Break
16:30-18:15 Session 34I: Regular talks, confluence competition (CoCo) and closing
Location: FH, Seminarraum 303
16:30
Normalization Equivalence of Rewrite Systems

ABSTRACT. Métivier (1983) proved that every confluent and terminating rewrite system can be transformed into an equivalent canonical rewrite system. He also proved that equivalent canonical rewrite systems which are compatible with the same reduction order are unique up to variable renaming. In this note we present simple and formalized proofs of these results. The latter result is generalized to the uniqueness of normalization equivalent reduced rewrite systems.

17:00
Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract)

ABSTRACT. This paper briefly sketches that "non-E"-overlapping and weakly-shallow TRSs are confluent" by extending reduction graph in our previous work (M.Sakai and M.Ogawa. Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent. Information Processing Letters vol.110, 2010) by introducing constructor expansion. A term is weakly shallow if each defined function symbol appears either at the root or in the ground subterms, and a TRS is weakly shallow if the both sides of rules are weakly shallow. The non-E-overlapping property is undecidable for weakly shallow TRSs and a decidable sufficient condition is the strongly non-overlapping condition. A Turing machine can be simulated by a weakly shallow TRS (p.27 in J.W.Klop, Term Rewriting Systems, 1993); thus the word problem is undecidable,in contrast to shallow TRSs.

17:30
Confluence Competition
SPEAKER: Harald Zankl

ABSTRACT. The 3rd Confluence Competition (CoCo 2014) runs live. The competition is part of the FLoC'14 Olympic Games.