-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: 24 July 2021 (Buenos Aires, Argentina, virtual) Chair: Cynthia Kop Co-Chair/Secretary: Carsten Fuhs -------------------------------------------------------------------------------- PARTICIPANTS Aart Middeldorp Alejandro Díaz-Caro Gilles Dowek Besik Dundua Carlos Gustavo López Pombo Carsten Fuhs Christopher Lynch Cynthia Kop Deepak Kapur Delia Kesner Femke van Raamsdonk Gilles Dowek Hans Zantema Jörg Endrullis (invited) Jürgen Giesl Luigi Liquori Malena Ivinsky Maribel Fernández Martin Avanzini Mauricio Ayala-Rincón (invited) Michał Gajda Nao Hirokawa Narciso Martí-Oliet Paliath Narendran Pietro Di Gianantonio René Thiemann Ricardo Oscar Rodríguez Roy Overbeek Salvador Lucas Sarah Winkler (invited) Silvia Ghilezan Stanislav Ignatiev Takahito Aoto Temur Kutsia Thaynara Delima Vincent van Oostrom Yuta Takahashi -------------------------------------------------------------------------------- AGENDA (1) Presentation Mauricio Ayala-Rincón (2) Presentation Jörg Endrullis (3) Presentation Sarah Winkler (4) Report on ISR 2021 (Madrid) by Narciso Martí Oliet (5) Reminder for ISR 2022 (Tbilisi) by Besik Dundua and Temur Kutsia (6) Discussion (7) Business Meeting (memberships, auxiliary topics) -------------------------------------------------------------------------------- (1) Presentation Mauricio Ayala-Rincón Title: Formalization of the Termination of Functional Specifications in PVS Abstract: This talk will present research on the formalization of automation of the termination for a functional language model called PVS0 designed for the meta-theoretical study of the PVS higher-order logic and its computational aspects. The PVS0 model is validated by proving its fundamental computability properties. Termination criteria related to PVS type-correctness conditions, size-change principle, calling-context and matrix-weighted graphs, and dependency pairs are specified. The correction of such termination criteria is guaranteed by formalizing their equivalence. (2) Presentation Jörg Endrullis Title: Graph Rewriting Abstract: There are various graph rewriting approaches based in category theory, for instance the well-known Double Pushout approach (DPO). We discuss some shortcomings of the existing frameworks, in particular concerning relabeling and control over the embedding in the context. We introduce a novel framework PBPO+ that overcomes these limitations. (3) Presentation Sarah Winkler Title: Decidable Fragments of First-order Logic via Termination of Rewriting Abstract: This talk presents new fragments of first-order logic whose decidability with respect to resolution techniques and the SGGS method is witnessed by existence of a suitable ordering on atoms. These fragments include the restrained, the sort-restrained, and the controlled class. Membership of a clause set in these classes can be tested by extracting a first-order term rewrite system from the clauses and proving it terminating with respect to rewriting or narrowing, using state-of-the-art automatic termination tools. The talk is partially based on the following paper: M.P. Bonacina and S. Winkler: SGGS Decision Procedures. In Proc. 10th IJCAR, volume 12166 of LNCS, pages 356-374, 2020. http://dx.doi.org/10.1007/978-3-030-51074-9_20 (4) Report on ISR 2021 (Madrid) by Narciso Martí Oliet Narciso Martí Oliet reported on ISR 2021, which was held online from 5 to 16 July 2021: The original plan had been to offer both a basic track and an advanced track in Madrid over one week in mid-July 2021. The state of the Covid-19 pandemic in Spring 2021 made clear that an on-site Summer School in July was not likely to be feasible. Running the basic track would require exercises and direct interaction, which would be difficult online. Cancelling ISR 2021 was considered. ISR 2019 organiser Frédéric Blanqui suggested that it would not be good to have no ISR for 2 years in a row and that ISR 2021 might run only the advanced track. Most of the planned speakers for ISR 2021 agreed to the following online setting: ISR 2021 was going to run over 2 weeks from 5 to 16 July with 11 courses (1 per day) of 3 hours per course in order to avoid screen fatigue. Some courses would run in the morning, some would run in the afternoon. The platform would be Zoom. Courses would be recorded for registered participants. Participation at ISR 2021 required free registration. There were over 180 registered participants, including speakers and organisers. Usually, there were 30 - 40 participants per course. There was little active participation, with few questions in general, but there was a show of interest. Some participants were unable not attend, but were interested in the recordings. The budget of ISR 2021 was EUR 6000. This has been used for the registration platform and for the Zoom licence. There was also a small payment for the speakers (some had preferred not to get it). David de Frutos provided funding. Thanks to: Frédéric Blanqui, helping colleagues (Albert Rubio, David de Frutos, ...), helping students, speakers, and participants. In the following discussion, Temur Kutsia asked for recommendations to future organisers and whether there had been unexpected problems. Narciso Martí Oliet pointed out that he had only little administrative support. For the future, in the basic track face-to-face teaching should be the best way. In the advanced track, at least some course could be online; possibly face-to-face and transmitted. Aart Middeldorp asked whether ISR 2021 had been evaluated by the participants, which could inform future participants. Narciso Martí Oliet said that this was still pending. Deepak Kapur asked how the topics for the technical programme had been decided. Narciso Martí Oliet pointed out that he had made an open call and then invited some other people for topics that had not been proposed. Vincent van Oostrom asked Narciso Martí Oliet which platform he would suggest for the future. Narciso Martí Oliet reported that the used platform Zoom was fine. Google Meet and Blackboard Collaborate had also been considered. Mauricio Ayala-Rincón stated that the school was very good and that he had sent students to specific advanced courses, but that basic courses were necessary, e.g., for MSc courses to raise interest in rewriting. He said that he was really satisfied with the courses and with the teaching/learning experience. Narciso Martí Oliet suggested that a basic online track might be feasible if it was not too long. (5) Reminder for ISR 2022 (Tbilisi) by Besik Dundua and Temur Kutsia Besik Dundua presented the plan for ISR 2022 at Tbilisi State University for the week of 19 to 26 September 2022. ISR 2022 would be part of CLAS 2022, the Computational Logic Autumn Summit. A number of events had already joined, PPDP/LOPSTR might join as well. Time plan for ISR 2022: - Beginning of Oct 2021: call for advanced courses - Nov 2021: deadline for course proposal submission - Dec 2021: notification, programme announcement - Jan 2022: publicity, call for participation - Jul 2022: registration deadline - End of Sep 2022: ISR 2022 The expected setting was hybrid, which should make it flexible to switch if needed. The university was going to provide rooms and facilities for free. It was planned to apply for sponsor money for CLAS 2022. There were no questions on ISR 2022. (6) Discussion Cynthia Kop pointed out that no proposals have arrived for ISR 2023 and asked whether ISR 2023 would take place. Narciso Martí Oliet responded that the topic had been discussed in the Steering Committee of ISR and that it was unclear whether it was good that ISR had taken place almost every year in recent years rather than every 2 years. Carsten Fuhs said that the bylaws stated that ISR should be organised at most every 2 years, giving some flexibility. (7) Business Meeting (memberships, auxiliary topics) Attendees: Carsten Fuhs Cynthia Kop Hans Zantema Aart Middeldorp Christopher Lynch Deepak Kapur Delia Kesner Femke van Raamsdonk Gilles Dowek Jürgen Giesl Luigi Liquori Maribel Fernández Nao Hirokawa René Thiemann Salvador Lucas Silvia Ghilezan Takahito Aoto The three invited speakers (Mauricio Ayala-Rincón, Jörg Endrullis, Sarah Winkler) were voted unanimously to be invited to join IFIP WG 1.6 via an open vote. The question how to deal with inactive members was raised, and the suggestion to ask inactive members whether they were still interested in the topic of the Working Group was made. The List Of Open Problems (LOOP) in Rewriting was discussed. It was identified that LOOP was currently somewhat outdated and that maintenance was the main issue. Hans Zantema stated that he had taken over from Ralf Treinen and that Nachum Dershowitz had later taken over, but not done anything with LOOP. He also pointed out that many problems in LOOP were not outdated. Several ways how a future maintainer could run LOOP efficiently were discussed. As the final point, the topic whether researchers in Rewriting still felt welcome at FSCD, which had also been raised at the General Meeting of FSCD 2021, was discussed. It was recognised that FSCD was significantly broader than the Rewriting-focused predecessor conference RTA. Conversely, papers on rewriting were now being published at a number of venues other than FSCD as well (e.g., CADE), which also listed Rewriting in their Calls for Papers.