---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 13, 2014 (Vienna, Austria) Chair: Juergen Giesl Secretary: Peter Schneider-Kamp more than 29 participants, including: Takahito Aoto (invited) Mauricio Ayala-Rincon Maria Paola Bonacina Roberto di Cosmo Nachum Dershowitz Dan Dougherty Gilles Dowek (invited) Maribel Fernandez Alfons Geser Juergen Giesl Nao Hirokawa (invited) Delia Kesner Gerwin Klein Florent Jacquemard (invited) Claude Kirchner Helene Kirchner Jose Meseguer Aart Middeldorp Georg Moser Vincent van Oostrom David Plaisted Femke van Raamsdonk Kristoffer Rose Dana Scott Sophie Tison Yoshihito Toyama Ralf Treinen Claus-Peter Wirth Hans Zantema ---------------------------------------------------------------------- Agenda: 1. Presentation by Takahito Aoto 2. International School on Rewriting (ISR) 3. Presentation by Gilles Dowek 4. Presentation by Maria Paola Bonacina 5. Presentation by Claude Kirchner and Discussion on Massive Open Online Courses and Overlay Journals 6. Presentation by Nao Hirokawa 7. Presentation by Florent Jacquemard 8. Discussion on the Future of RTA 9. Discussion on the List of Open Problems in Rewriting 10. Business Meeting ---------------------------------------------------------------------- 1. Takahito Aoto and Sorin Stratulat: Decision Procedures for Proving Inductive Theorems without Induction 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. ---------------------------------------------------------------------- 2. Aart Middeldorp: International School on Rewriting (ISR) * Aart Middeldorp (ISR SC Chair): Overview on the history and organisation of ISR * Mauricio Ayala-Rincon: Report on ISR 2014 - Carlos Castro is the main organizer of ISR 2014 - Mauricio Ayala-Rincon is a member of the organization committee. - ISR will take place on August 25-29 in Valparaiso, Chile - a week before WoLLIC (which is on September 1-4). - The lecturers for the basic track will be Aart Middeldorp and Sarah Winkler. The lecturers for the advanced track will be Mauricio Ayala-Rincon, Eduardo Bonelli, Claude Kirchner, Helene Kirchner, Pierre-Etienne Moreau, Camilo Rocha, and Johannes Waldmann. - The lecturers have to pay their trips themselves, but the organizers pay the local costs. - The registration fee for students is 300 US$ for early registrations and 400 US$ for late registrations. - Up to now there are very few registrations (6 for the basic track and 5 for the advanced track). The goal is to obtain at least 10 participants for each track. - The problem is that students only get funding if they have a poster or talk at the school. To solve this, the school could include a poster session where students can present their posters. - Aart Middeldorp suggests to include exams for the beginner track such that students can obtain credits for their studies. However, Mauricio Ayala-Rincon does not think that there will be exams at ISR 2014. * Alfons Geser: Report on ISR 2015 - Alfons Geser and Johannes Waldmann will organize ISR 2015 in Leipzig, Germany. - There will again be a basic track (with Aart Middeldorp as lecturer) and an advanced track. A call for proposals for the advanced track has been issued. - The date will be August 10-14, 2015. This is a week after CADE in Berlin. - The date conflicts with the date of the ESSLLI summer school. - The registration fee for students will be 300 Euro. - Claude Kirchner suggests to make the material from the lectures freely available and to use it for MOOCs. Alfons Geser has objections since then this material could be accessed without fees. Gilles Dowek suggests that lecturers should give their courses twice (once for the students at ISR and once for a video recording that is made available online). * Gerwin Klein: Proposal for ISR 2016 in Sydney, Australia - The proposal is to organize ISR 2016 in Sydney. The organizer would be Gabriele Keller (University of New South Wales, UNSW) - The UNSW is one of Australia's top universities with more than 50,000 students. - ISR could be held on campus, where seminar rooms would be available for free. - The university is located near the city center and the beach. It is easy to reach by public transport. - There are many restaurants nearby with lunch for approx. 10 AUS$. - The basic track would be held as a UNSW course. There would be assignments during the course and an exam after ISR. - Accommodation would cost around 60-80 AUS$. - The proposed date would be the last week of February or the week of July, 17. The date should be left open until the dates of conferences in the same period is known. - A registration fee for students only has to be imposed if the lecturers need funding. - There will also be (some) lecturers from Australia. UNSW and NICTA offer a lot of expertise in formal methods, verification, and functional programming. - No co-location with other workshops or schools is currently planned. - Video recording of the lectures might be possible. - The proposal is accepted unanimously by the audience. ---------------------------------------------------------------------- 3. Gilles Dowek and Ying Jiang: Rewriting, Proofs and Transition Systems We give a new proof of the decidability of reachability in alternating pushdown systems, showing that it is a simple consequence of a cut-elimination theorem for some logic. ---------------------------------------------------------------------- 4. Maria Paola Bonacina and David Plaisted: Semantically-Guided Goal-Sensitive Theorem Proving SGGS, for Semantically-Guided Goal-Sensitive theorem proving, is a new inference system for first-order logic. It was inspired by the idea of generalizing to first-order logic the model-based style of the Davis-Putnam-Logemann-Loveland (DPLL) procedure for propositional logic. Model-based reasoning is a key feature of SAT solvers, SMT solvers, and model-constructing decision procedures for specific theories, and a crucial ingredient to their practical success. However, model-based reasoning in first-order logic is challenging, because the logic is only semi-decidable, 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 model-based 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 first-order problems; goal-sensitive, 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 model-centric 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 first-order logic with equality, which requires rewrite-based reasoning. A manuscript including all aspects of SGGS, the technical details, the proofs of refutational completeness and goal-sensitivity, a comparison with other work (e.g., resolution with set of support, the disconnection calculus, the model evolution calculus, the Inst-Gen method) and more references, is available. ---------------------------------------------------------------------- 5. Claude Kirchner: Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing - The talk is followed by a discussion on massive open online courses and overlay journals. - Existing academic social networks like Mendeley and ResearchGate are presented and discussed. - Claude Kirchner reports on the EPISCIENCES platform implemented by INRIA to create overlay journals on top of public archives like arXiV and HAL. - Here, authors put their papers on public archives and then ask an editorial board of an overlay journal to evaluate it. Following the reviews, the authors can revise their paper, but all versions remain accessible to the public. Final accepted versions are marked accordingly. ---------------------------------------------------------------------- 6. Nao Hirokawa, Aart Middeldorp and Georg Moser: Basic Normalization The Normalization Theorem (O'Donnell 1977) states that for every left-normal 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 left-normality condition rules out many functional programs. We revisit the problem to seek a solution for normalization of the leftmost outermost strategy. ---------------------------------------------------------------------- 7. Florent Jacquemard, Jean Bresson and Pierre Donat-Bouillud: Rhythm Tree Rewriting 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. ---------------------------------------------------------------------- 8. Georg Moser: Discussion on the Future of RTA - There is concern about the lack of application papers at RTA. - At RTA 2015, there should be 3 categories for papers: full papers, system descriptions, and application papers. - Juergen Giesl remarks that a similar discussion already took place at the last meeting of the IFIP WG 1.6 and that the steering committee had agreed to inform Gilles Dowek (the PC Chair of RTA 2014) accordingly, but nothing had happened. - Jean-Pierre Jouannaud instead suggests to invite researchers to RTA in order to extend rewriting to new directions. - Gilles Dowek would like to clarify what is meant by "applications" in this context. - Juergen Giesl states that clear criteria are needed to define what is expected from papers in the different categories. These criteria are needed both for the authors and the referees. - Jean-Pierre Jouannaud remarks that the reviews at RTA are often harsher than at other more prestigious conferences. - It is discussed whether there should be quotas for application papers, but Georg Moser is not in favor of it. - Kristoffer Rose points out that application papers should not be marked as such in the proceedings. They should have the same status as full papers. - Helene Kirchner says that that there are areas that use rewriting, but whose topics are very far away from RTA. It is not clear why RTA should attract these papers. - Jose Meseguer mentions that we should also be open for new research directions. - Gilles Dowek thinks that potential authors hardly read the call-for-papers. One should rather focus on certain applications (e.g., bio-informatics or music) and address people from these areas directly. - Nachum Dershowitz discusses the potential restriction that PC members may only submit application papers. - Maribel Fernandez suggests to highlight a certain sub-area each year for RTA. ---------------------------------------------------------------------- 9. Nachum Dershowitz & Hans Zantema: Open Problems in Rewriting - Hans Zantema explains the list of open problems in rewriting which exists since RTA 1995. - Since 2012, Hans Zantema maintains the list (he took it over from Ralf Treinen). - Ralf Treinen had developed a system for automating tasks concerned with the maintenance of the list, but this is difficult to use for others. - Nachum Dershowitz asked his admins who managed to get the system running again. - In the last years, there were no reactions and no new problems submitted. Most of the problems are from the 90s. - Nachum Dershowitz suggests to switch to a wiki-system with a moderator. - Jean-Pierre Jouannaud thinks that someone should write a paper on the open problems of the last RTA(s). - Gilles Dowek suggests to mark the 5 most important open problems on the list. - Ralf Treinen asks which motivation people could have to submit open problems. They might do it in order to get cited. - Gilles Dowek remarks that open problems should be clear questions and not problems that just require that some topic should be investigated. - The audience votes the suggestion to switch to a wiki-system. There are 9 Yes votes, 3 No votes, and 1 Abstain vote. Nachum Dershowitz takes the initiative and will be the moderator of the wiki. ---------------------------------------------------------------------- 10. Juergen Giesl: Business Meeting - Nao Hirokawa is invited as a new member to the WG after having been invited to the meetings in 2012 and 2014. - Florent Jacquemard is invited as a new member to the WG after having been invited to the meetings in 2013 and 2014. - Before the meeting in 2013, the strict rule was announced that the membership expires for members who are not present at 3 meetings in a row. Therefore, members who do not attend any of the meetings in 2013, 2014, and 2015 will be removed from the WG after the meeting in 2015. - Those member that are "at risk" (i.e., who would be removed if they do not attend the meeting in 2015) should be informed by email well in advance before the meeting in 2015. In this way, they can still attend the meeting in order to remain in the WG. - There is an unanimous vote that the next IFIP WG 1.6 meeting should take place at RTA/TLCA in June 2015 in Warsaw, Poland. - Juergen Giesl reports on the IFIP conferences. - Since Juergen Giesl's second term as chair of the WG expires this year, he cannot be re-elected anymore. He will therefore organize the election of the next chair of the WG this fall. - Jose Meseguer suggests to discuss over the email list who might become honorary member instead of being removed from the WG. - Juergen Giesl suggests to contact researchers that would be removed and if they are really still interested in rewriting, one could offer them to stay in the WG. - Georg Moser would like to have more young people in the WG. - Kristoffer Rose and Georg Moser would like the WG to take over the rewriting homepage. ----------------------------------------------------------------------