# Selected papers of the joint 26th International Conference on "Rewriting Techniques and Applications" and 13th International Conference on "Typed Lambda Calculi and Applications" RTA/TLCA 2015

Editors: Thorsten Altenkirch, Maribel Fernández

### 1. Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic $\mathcal{EL}$ to disunification since negative constraints can be used to avoid unwanted unifiers. While […]

### 2. On linear rewriting systems for Boolean logic and some applications to proof theory

Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In […]

### 3. Termination of Cycle Rewriting by Transformation and Matrix Interpretation

We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination […]

### 4. Reachability Analysis of Innermost Rewriting

We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs, and several rewriting tools exist for solving this problem. […]

### 5. Certifying Confluence Proofs via Relative Termination and Rule Labeling

The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on […]