View: session overviewtalk overviewside by side with other conferences
08:45  Decision Procedures for Proving Inductive Theorems without Induction SPEAKER: Takahito Aoto ABSTRACT. Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive reasoning. In this talk, a new approach for deciding inductive theorems of TRSs is described. In particular, we give procedures for deciding the inductive validity of equations in some standard TRSs on natural numbers and lists. Our essential idea is to use the validity in the initial algebras of TRSs, instead of validity guaranteed by existence of inductive proofs. Contrary to previous decidability results, our procedures can automatically decide without involving induction reasoning the inductive validity of arbitrary equations for these TRSs, that is, without imposing any syntactical restrictions on the form of equations. 
09:15  Discussion on the International School on Rewriting (ISR) SPEAKER: Aart Middeldorp ABSTRACT.

10:45  Rewriting, Proofs and Transition Systems SPEAKER: Gilles Dowek ABSTRACT. We give a new proof of the decidability of reachability in alternating pushdown systems, showing that it is a simple consequence of a cutelimination theorem for some logic. 
11:30  SemanticallyGuided GoalSensitive Theorem Proving SPEAKER: Maria Paola Bonacina ABSTRACT. SGGS, for SemanticallyGuided GoalSensitive theorem proving, is a new inference system for firstorder logic. It was inspired by the idea of generalizing to firstorder logic the modelbased style of the DavisPutnamLogemannLoveland (DPLL) procedure for propositional logic. Modelbased reasoning is a key feature of SAT solvers, SMT solvers, and modelconstructing decision procedures for specific theories, and a crucial ingredient to their practical success. However, modelbased reasoning in firstorder logic is challenging, because the logic is only semidecidable, the search space is infinite, and model representation is harder than in the propositional case. SGGS meets the challenge by realizing a seemingly rare combination of properties: it is modelbased a la DPLL; semantically guided by an initial interpretation, to avoid blind guessing in an infinite search space; proof confluent, to avoid backtracking, which may be cumbersome for firstorder problems; goalsensitive, which is important when there are many axioms or a large knowledge base; and it uses unification to avoid enumeration of ground terms, which is inefficient, especially for rich signatures. In terms of operations, SGGS combines instance generation, resolution, and constraints, in a modelcentric approach: it uses sequences of constrained clauses to represent models, instance generation to extend the model, resolution and other inferences to repair it. This talk advertises SGGS to the rewriting community, presenting the main ideas in the method: a main direction for future work is extension to firstorder logic with equality, which requires rewritebased reasoning. A manuscript including all aspects of SGGS, the technical details, the proofs of refutational completeness and goalsensitivity, a comparison with other work (e.g., resolution with set of support, the disconnection calculus, the model evolution calculus, the InstGen method) and more references, is available. 
12:00  Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing SPEAKER: Claude Kirchner 
12:30  Discussion on Massive Open Online Courses and Overlay Journals SPEAKER: Claude Kirchner 
14:30  Basic Normalization SPEAKER: Nao Hirokawa ABSTRACT. The Normalization Theorem (O'Donnell 1977) states that for every leftnormal orthogonal rewrite system, the leftmost outermost strategy reduces any term to the normal form if it exists. Although the theorem ensures the normalization property of important systems like Combinatory Logic, the leftnormality condition rules out many functional programs. We revisit the problem to seek a solution for normalization of the leftmost outermost strategy. 
15:15  Rhythm Tree Rewriting SPEAKER: Florent Jacquemard ABSTRACT. In traditional western music notation, the durations of notes are expressed hierarchically by recursive subdivisions. This led naturally to a tree representation of melodies widespread in systems for assistance to music authoring. We will see how term rewriting techniques can be applied to computer music problems, in particular to the problem of rhythm quantization: the transcription of a sequence of dates (real time values) into a music score. Besides the question of rhythm representation, an interesting problem in this context is the design and concise description of large rewrite rule sets and decision problems for these descriptions. 
16:30  Discussion on the Future of RTA (+ TLCA) SPEAKER: Georg Moser 
17:00  Discussion on the Open Problems List in Rewriting SPEAKER: Nachum Dershowitz 
17:30  Business Meeting SPEAKER: Jürgen Giesl 