---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 19, 2025 (Birmingham, UK) Chair: Cynthia Kop Secretary: Carsten Fuhs Minutes by: Juergen Giesl ---------------------------------------------------------------------- Agenda: 1. Presentation by Raúl Gutiérrez (Invited) 2. Presentation by Santiago Escobar (Invited) 3. Presentation by Florian Frohn (Invited) 4. Presentation by Daniele Nantes (Invited) 5. Update on the International School on Rewriting (Cynthia Kop) 6. Presentation by David Cerna (Invited) 7. Business Meeting ---------------------------------------------------------------------- 1. Raúl Gutiérrez: How Infeasibility Can Help Prove Computational Properties of Term Rewriting Systems In the realm of term rewriting, given terms s and t, a reachability condition is said to be feasible if there exists a substitution such that s rewrites to t in zero or more steps; otherwise, it is called infeasible. Checking the infeasibility of (sequences of) reachability conditions is important in analyzing computational properties of rewrite systems, such as confluence or (operational) termination. In this talk, we show how infeasibility can be introduced in the automatic analysis of computational properties of variants of term rewriting system. Furthermore, we present how a more general notion of feasibility enables more advanced analyses, allowing us to prove properties of more complex systems, such as Maude theories. ---------------------------------------------------------------------- 2. Santiago Escobar: NuITP: An Inductive Theorem Prover for Maude NuITP is an inductive equational theorem prover for Maude equational theories that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms). Maude equational theories include expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms. This talks presents the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark. ---------------------------------------------------------------------- 3. Florian Frohn: Symbolic Under-Approximations Traditionally, research on verification has a stronger focus on proving rather than disproving properties like termination or safety. While proving such properties requires over-approximations, under-approximating reasoning is needed to disprove them. Similarly, most techniques for worst-case complexity analysis are based on over-approximations and thus yield upper instead of lower bounds. In this talk, we survey various approaches for computing symbolic under-approximations for rewrite and transition systems that approximate reductions of arbitrary length, and give rise to state-of-the-art techniques for proving non-termination unsafety, and worst-case lower bounds. ---------------------------------------------------------------------- 4. Daniele Nantes: Equational Reasoning in Languages with Binders Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and alpha-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in alpha-equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the pi-calculus. Joint work with Ali K. Caires-Santos and Maribel Fernández. ---------------------------------------------------------------------- 5. Cynthia Kop: Update on the International School on Rewriting Cynthia presents an update on ISR to be organized directly before FLoC in Nijmegen, The Netherlands in July 2026. ---------------------------------------------------------------------- 6. David Cerna: Anti-unification and the Lambda Cube: Results and Next Steps Anti-unification (AU), also known as generalization, is a fundamental operation used for inductive inference. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. While most investigations focus on the first-order or equational variants, there have been a few developing algorithms for higher-order variants and investigating applications of existing procedures. Recent investigations focused on the simply-typed lambda calculus, but considering generalizations from fragments beyond patterns. In this talk, we discuss this recent work, open problems, and next steps to generalize the results to more expressive type systems of the lambda cube. ---------------------------------------------------------------------- 7. Business Meeting Participants in Presence: Juergen Giesl Cynthia Kop Jose Meseguer Naoki Nishida Vincent van Oostrom Femke van Raamsdonk Participants via Zoom: Sandra Alves Mauricio Ayala-Rincon Maribel Fernandez Carsten Fuhs Nao Hirokawa Delia Kesner Teimuraz Kutsia Luigi Liquori Christopher Lynch - Santiago Escobar and Daniele Nantes have given two invited talks at meetings of the IFIP WG. The WG agrees unanimously to invite them as new members to the working group. - New bylaws * Principles for new bylaws had been agreed upon at the last meeting of the IFIP WG. * Cynthia had prepared the bylaws and sent them around via e-mail in advance. * Femke summarizes the main contents of the bylaws at the meeting. * There is discussion that "active" members should be the same as "regular" members. * The idea is that regular/active members may not miss 3 consecutive business meetings, whereas honorary members do not have any such duties. * It should be checked how our regulations correspond to the general IFIP-regulations and if needed, the bylaws can again be adapted and voted upon at the next meeting. * The new bylaws are accepted and ratified unanimously by the WG. - Jose proposes to add an emeritus status to the bylaws. * This corresponds to the status of "honorary members". * There is discussion whether this status should be offered to all members when reaching retirement. * This should be voted upon at the next meeting. - Luigi reports on the new rewriting website * The old website by Nachum Dershowitz and Laurent Vigneron in Nancy still exists, but many links are broken (http://rewriting.loria.fr/). * Since 2023, Luigi is working on a new reshaped website (https://rewriting.inria.fr). * The new website can be modified by people with a corresponding login password. * Luigi and Nachum will transfer the content from the old to the new website, then the old website in Nancy will be closed. The WG agrees with this unanimously. * After Luigi's retirement, the new website will continue to work. * There is discussion about using a wiki instead of a classic website. * We should also ensure that Wikipedia's website for rewriting is kept up-to-date (https://en.wikipedia.org/wiki/Rewriting) * The list of open problems in rewriting should also move to the new rewriting website. It should not be merged with the TLCA list of open problems. * The rewriting mailing list (maintained by Pierre Lescanne) may also move to the location of the new website. Luigi is investigating this possibility. - If there are sufficiently many new items to decide upon (e.g., concerning the bylaws or the website), then there can be an online meeting on demand before the next regular meeting in one year. - The next regular meeting of the IFIP WG should be in Lisbon during FLoC 2026.