arXiv:2509.23739v1 [cs.LO] 28 Sep 2025
|
DOI:
10.4204/EPTCS.430 ISSN: 2075-2180 |
This volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasília, the capital of Brazil, from October 7 to October 8, 2025.
The aim of the LSFA series of workshops is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory.
The 20th International Workshop on Logical and Semantic Frameworks with Applications continues the successful workshops held in Natal (2006), Ouro Preto (2007), Salvador (2008), Brasília (2009), Natal (2010), Belo Horizonte (2011), Rio de Janeiro and Niterói (2012), São Paulo (2013), Brasília (2014), Natal (2015), Porto (2016), Brasília (2017), Fortaleza (2018), Natal (2019), Bahia (2020), Buenos Aires (virtual) (2021), Belo Horizonte (2022), Rome (2023), and Goiânia (2024).
For LSFA 2025, seven contributions were accepted out of eleven submissions, with three or four reviewers per submission. Among the seven accepted submissions, five regular papers were accepted for inclusion in this volume and two submissions were accepted as presentation-only contributions.
In addition, the program included three invited talks given by Temur Kutsia (Research Institute for Symbolic Computation, Johannes Kepler University), Bruno Lopes (Instituto de Computação, Universidade Federal Fluminense), and Yoni Zohar (Department of Computer Science, Bar Ilan University).
Temur Kutsia's presentation was a joint invited talk with CICM 2025.
Many people helped to make LSFA 2025 a successful event. We would like to thank all the PC members, the additional subreviewers, and the LSFA 2025 organizers.
Haniel Barbosa, Christophe Ringeissen (LSFA 2025 PC co-chairs)
Symbolic constraint solving is a fundamental technique in many areas of mathematics and computer science, providing the basis for key operations in automated reasoning, term rewriting, declarative programming, or formal methods. Important classes of symbolic constraints include unification, matching, generalization, disunification, ordering constraints. Efficient methods for solving them form the computational core of inference engines, proof assistants, program transformation systems, logical frameworks, etc.
In this talk, we present recent advances in solving unification, matching, and generalization constraints in expressive theories, including those that involve background knowledge or binding constructs. We discuss algorithmic techniques for constraint solving, identify classes of problems that admit efficient solutions, and highlight their relevance for tools and techniques in symbolic computation and computer mathematics.
Propositional Dynamic Logic (PDL) is a sophisticated modal logic tailored to reason about programs. Several fragments and extensions of PDL are worth studying, allowing us to control complexity or increase expressiveness.
By limiting PDL to deterministic fragments, such as Deterministic PDL or Strictly Deterministic PDL, we introduce new program behaviors by excluding nondeterministic choices or restricting the form of iteration. These restrictions affect both expressiveness and computational complexity. While standard PDL is decidable and has an EXPTIME-complete satisfiability, some deterministic fragments have lower complexity bounds, such as PSPACE-complete. It is a showcase of a trade-off between expressiveness and tractability.
Conversely, attempts to increase expressiveness come with significant challenges. Extensions like Context-Free PDL result in undecidable validity. This discussion will explore the effects of restricting to deterministic programs and examine how to enhance expressiveness using memory.
Theory combination in Satisfiability Modulo Theories (SMT) deals with the generation of algorithms for combinations of theories, based on the algorithms for each of the specific theories being combined.
Among the most important combination methods is the polite combination method, which has two major advantages: first, it only requires solvers for the theories being combined, and no other mechanism is needed (e.g., there is no need for an algorithm that computes cardinalities of models). Second, it only requires one of the theories to admit some property, while the other only has to be decidable.
When polite combination was introduced, it was claimed that the required property is politeness (a notion I will formally and intuitively describe in my talk). But, later, it was shown that the correctness proof had a bug, and for the proof to work, a stronger property is needed to be assumed, namely strong politeness.
Hence, while the importance of the polite combination method is unquestionable (its incorporation in the state-of-the-art solver cvc5 is a case in point), it was left unclear what is the value of the politeness property. Can it still be considered a property that is relevant to theory combination?
In this talk I will describe several attempts made by myself and others to answer this question positively, thus saving the politeness property.
No background in theory combination or SMT is assumed, though politeness is expected.
Reasoning about equality modulo equational theories in languages with variable binding requires careful handling of names, freshness, and \(\alpha \)-equivalence. The nominal approach provides a solid framework with applications in unification, rewriting, and universal algebra. Recent work replaces traditional freshness constraints with permutation fixed-point constraints scoped by the quantifier \(|\!/\!|\), ranging over fresh names. Based on this framework, we define a proof system and discuss its soundness and completeness with respect to nominal set semantics. Unlike in the original nominal algebra, this system does not satisfy the classical HSP theorem because homomorphic images may fail to preserve fixed-points. We explore restricting homomorphisms to those preserving fixed-points to recover an HSP-like result. This talk presents these ideas and discusses open problems.
Equality plays a central role in algebra and logic, but in the \(\lambda \)-calculus it is complicated not only by variable binding and freshness conditions but also by the higher-order nature of the system and in extensions such as the \(\eta \)-rule. For example, the \(\eta \)-rule (\(\lambda x.(Mx) = M\) when \(x\) is not free in \(M\)) relies on distinguishing bound and free variables, as well as between object-level (like \(x\)) and meta-level variables (like \(M\)).
To address such challenges, three major paradigms for representing bindings have been developed: De Bruijn indices, higher-order abstract syntax (HOAS), and the nominal approach. Among these, the nominal approach introduced by Gabbay and Pitts [6] provides an explicit and flexible treatment of names and binding, supporting \(\alpha \)-equivalence, freshness, and name generation in a way that aligns closely with mathematical practice. Since then, nominal techniques have been applied across several domains such as unification [7], rewriting [3], and universal algebra [5].
In these domains, nominal terms play a central role by presenting a two-level syntax constructed from a countably infinite set of atoms \(\mathbb {A} = \{a,b,c,\ldots \}\) representing object-level variables, a countably infinite set of unknowns \(\mathbb {V} = \{X,Y,Z,\ldots \}\) representing meta-level variables, function symbols \(\mathtt {f}\), and name abstractions \([a]t\). The abstraction \([a]t\) models the binding of the atom \(a\) in the term \(t\), similar to variable binding in expressions like \(\lambda x.t\) or \(\forall x.\phi \). Formally, terms are given by the grammar: \[ t,u ::= a \mid \pi \cdot X \mid \mathtt {f}(t_1, \ldots , t_n) \mid [a]t \] where \(\pi \cdot X\) is a suspension applying a finite permutation \(\pi \) from the group \({\mathcal {G}}(\mathbb {A})\) of atom permutations to a meta-variable \(X\). When \(\pi = \mathtt {id}\), we simply write \(X\). Intuitively, suspensions can be read as "permute as \(\pi \) in whatever \(X\) becomes". The framework also includes freshness constraints, denoted \(a \# t\), which generalize the notion of "does not occur free". When \(t \equiv X\), such constraints are called primitives.
Nominal universal algebra [5] builds on the syntax of nominal terms to define a proof system for reasoning about equality modulo an equational theory \(\mathtt {T}\), while incorporating \(\alpha \)-equivalence. It also studies the models of this reasoning through nominal sets: sets equipped with an action of the group \({\mathcal {G}}(\mathbb {A})\), where each element \(x\) has a finite set of atoms it depends on, called its support, denoted by \(\mathtt {supp}_{}(x)\). Freshness constraints are interpreted semantically by the relation \(a {\#}_{\mathtt {sem}} x\), which holds if and only if \(a \notin \mathtt {supp}_{}(x)\). Alternatively, freshness can be intuitively understood as a combination of the quantifier \(|\!/\!|\) and fixed-point equalities under atom swapping. Formally, semantic freshness can be expressed as (see [6, Eq. 13]): \(a{\#}_{\mathtt {sem}} x\) if and only if \(|\!/\!| \mathbf {c}.(a \ \mathbf {c}) \cdot x = x\), where the quantifier \(|\!/\!|\mathbf {c}.P(\mathbf {c})\) means that the property \(P(\mathbf {c})\) holds for all but finitely many atoms \(\mathbf {c}\).
Semantic freshness can be seen as a negative condition: \(a {\#}_{\mathtt {sem}} x\) means that the atom \(a\) is not in the support of \(x\). Fixed points rephrase this in a more positive way: an atom \(a\) is fresh for \(x\) when it stays the same after swapping \(a\) with all but finitely many other atoms. This shift is interesting because many properties we care about in algebra and logic, such as commutativity, are described as invariances, not absences.
Seeing freshness as invariance explains why \(a\) is fresh for an element, instead of just stating it. For example, \(a\) is fresh for \(x = \mathtt {f}(b,d)\) not only because \(a\) is absent from the support \(\mathtt {supp}_{}(x) = \{b,d\}\), but also because swapping \(a\) with any other fresh atom \(\mathbf {c}\) leaves the term unchanged: \((a \ \mathbf {c})\cdot \mathtt {f}(b,d) = \mathtt {f}(b,d)\). This invariance perspective allows us to decide freshness without knowing the exact support of \(x\). It is enough to know that \(x\) has a finite support: if \(x\) remains unchanged under swaps of \(a\) with all but finitely many other atoms, then \(a\) cannot be in its support. This simplifies reasoning, because we no longer need to track precisely which atoms occur in \(x\).
This inspired the work of Ayala et al. [1] who proposed replacing primitive freshness constraints \(a \# X\) with primitive fixed-point constraints of the form \(\pi \cdot X \overset {}{\approx }_{\mathtt {C}} X\), abbreviated as \(\pi \curlywedge _{\mathtt {C}} X\), where \(\pi \) is an arbitrary finite permutation. This approach directly captures the invariance view of freshness. However, a limitation of this approach is that when these constraints are not scoped under a \(|\!/\!|\)-quantifier, they do not fully capture the standard nominal semantics of freshness. For instance, even though \((a \ b) \cdot (a + b) =_{\mathtt {C}} a + b\) holds, neither \(a\) nor \(b\) is fresh for \(a + b\).
To address this, the approach in [2] extends [1] by introducing nested \(|\!/\!|\)-quantification over fixed-point constraints of the form \(|\!/\!|\mathbf {\overline {c}}.\pi \curlywedge _{\mathtt {C}} X\), where the list \(\mathbf {\overline {c}}\) includes atoms that may occur in the permutation \(\pi \). This design takes advantage of the fact that every finite permutation admits a canonical decomposition into disjoint cycles. Using this, any permutation \(\pi \) appearing in a constraint \(|\!/\!|\mathbf {\overline {c}}. \pi \curlywedge _{\mathtt {C}} X\) can be split as \(\pi = \pi _{\mathbf {\overline {c}}} \circ \pi _{\neg \mathbf {\overline {c}}}\), where \(\pi _{\mathbf {\overline {c}}}\) includes all cycles that involve at least one atom from \(\mathbf {\overline {c}}\), and \(\pi _{\neg \mathbf {\overline {c}}}\) includes the remaining cycles. Since these cycles act on disjoint sets of atoms, the permutations \(\pi _{\mathbf {\overline {c}}}\) and \(\pi _{\neg \mathbf {\overline {c}}}\) have disjoint domains, making this factorization well-defined and unique. For example, in the constraint \(|\!/\!|\mathbf {c_1},\mathbf {c_2}. (a \ \mathbf {c_1} \ d)\circ (e \ f) \circ (g \ \mathbf {c_2})\curlywedge _{\mathtt {C}} X\), we have \(\pi _{\mathbf {\overline {c}}} = (a \ \mathbf {c_1} \ d) \circ (g \ \mathbf {c_2})\) and \(\pi _{\neg \mathbf {\overline {c}}} = (e \ f)\).
An important feature of this framework is that such constraints satisfy the equivalence: \(|\!/\!|\mathbf {\overline {c}}. \pi \curlywedge _{\mathtt {C}} X\) if and only if \(|\!/\!|\mathbf {\overline {c}}.(\pi _{\mathbf {\overline {c}}} \curlywedge _{\mathtt {C}} X\wedge \pi _{\neg \mathbf {\overline {c}}}\curlywedge _{\mathtt {C}}X)\). This shows that \(|\!/\!|\)-quantified fixed-point constraints extend primitive freshness: they can be viewed as a combination of freshness-like constraints (captured by \(\pi _{\mathbf {\overline {c}}}\)) and invariant, "pure" fixed-points (captured by \(\pi _{\neg \mathbf {\overline {c}}}\)).
It is worth noting that one practical advantage of fixed-point constraints is that because they can be seen as a special case of equality between nominal terms, the proof system can rely solely on equality rules. Unlike freshness constraints, we do not need a separate set of rules for relations like \(a \# X\).
A limitation of previous works is that they have focused on specific equational theories such as commutativity (\(\mathtt {C}\)), associativity (\(\mathtt {A}\)), and associativity-commutativity (\(\mathtt {AC}\)). In this talk, we take a further step by presenting a proof system for term equality modulo \(\alpha \)-equivalence and an arbitrary equational theory \(\mathtt {T}\), based on \(|\!/\!|\)-quantified permutation fixed-point constraints. This approach integrates ideas from nominal algebra [5] and recent developments in reasoning modulo commutativity [2]. In this talk, we will outline these notions and discuss the main ideas and recent advances regarding the soundness and completeness of this system, providing a conceptual foundation for reasoning in a broader class of theories.
Going back to the framework of freshness constraints, we see that it provides not only a syntax and a proof system, but also a solid algebraic foundation. In fact, it extends some classical results from universal algebra, such as the HSP theorem (Homomorphisms, Subalgebras, Products). The nominal version of HSP [4] says that classes of nominal algebras that are closed under homomorphic images, subalgebras, products, and atom abstraction are exactly the ones that can be described by equations. This gives us a useful link between syntactic reasoning (equations with freshness) and semantic closure properties.
Freshness constraints in the original nominal algebra may initially seem outside the scope of equational reasoning. However, the nominal HSP theorem shows that they admit an algebraic characterization. This result allows the original system based on freshness to qualify as a universal algebra in the classical sense. In this talk, we investigate whether a similar characterization can be established for the extended system based on \(|\!/\!|\)-quantified fixed-point constraints.
Our current findings indicate that the standard formulation of the HSP theorem fails for this extended setting. Intuitively, this happens because surjective homomorphisms between algebras can identify elements that are not equal in the domain, which may cause fixed-point conditions to hold in the codomain even when they do not in the domain. To address this issue, we propose to restrict attention to rigid homomorphisms, that is, those that preserve fixed-points, as a potential path to recovering a meaningful HSP-style result. The talk will outline this problem and key open questions.
[1] Mauricio Ayala-Rincón, Maribel Fernández & Daniele Nantes-Sobrinho (2020): On Nominal Syntax and Permutation Fixed Points. Log. Methods Comput. Sci. 16(1), p. 19:1-19:36, doi:10.23638/LMCS-16(1:19)2020.
[2] Ali K. Caires-Santos, Maribel Fernández & Daniele Nantes-Sobrinho (2025): Equational Reasoning Modulo Commutativity in Languages with Binders. In: Proceedings of the 30th International Conference on Automated Deduction (CADE-30), Lecture Notes in Computer Science, Springer, pp. 632-652, doi:10.1007/978-3-031-99984-0_33. Extended version available at arXiv:2502.19287.
[3] Maribel Fernández & Murdoch James Gabbay (2007): Nominal Rewriting. Inf. Comput. 205(6), pp. 917-965, doi:10.1016/j.ic.2006.12.002.
[4] Murdoch James Gabbay (2009): Nominal Algebra and the HSP Theorem. J. Log. Comput. 19(2), pp. 341-367, doi:10.1093/logcom/exn055.
[5] Murdoch James Gabbay & Aad Mathijssen (2009): Nominal (Universal) Algebra: Equational Logic with Names and Binding. J. Log. Comput. 19(6), pp. 1455-1508, doi:10.1093/logcom/exp033.
[6] Murdoch James Gabbay & Andrew M. Pitts (2002): A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput. 13(3-5), pp. 341-363, doi:10.1007/s001650200016.
[7] Christian Urban, Andrew M. Pitts & Murdoch James Gabbay (2004): Nominal Unification. Theor. Comput. Sci. 323(1-3), pp. 473-497, doi:https://10.1016/j.tcs.2004.06.016.
Termination is an essential property for term rewrite systems and is
necessary for completion procedures, which are widely studied and known
in first-order. However, when working with languages with binders, one
has to reason modulo alpha-equivalence and handle freshness conditions.
In addition, these have to be integrated into rewriting derivations, adding
challenges to the process. This challenge becomes greater when we add an
equational theory to the reasoning, especially when we have axioms that
may not be oriented without losing termination: such as Commutativity.
This paper presents a generalisation of the recursive path ordering modulo
\(\alpha \)-equivalence and permutation equations (specifically the commutative
one), in order to build a completion procedure that will work whenever
one has confluence modulo \(C\).
Abstract
When studying term rewriting systems, one property that is often sought is termination. Even though termination is undecidable in general, we can show that a particular rewriting system terminates using reduction order. Basically, if we can show that \(l > r\) for all system rules of the form \(l \to r\), given some specific reduction order \(>\), then the rewriting system is terminating. The only thing left to do is to find a specific order that works for the rewriting system in question. The real challenge is to find a reduction order that works with as many systems as possible.
One of the best-known reduction orders used in first-order term rewriting systems is Recursive Path Ordering (RPO) [3], which can be used in fully automated termination proofs [2]. Essentially, the idea of RPOs involves initially comparing the root symbols of two terms, followed by a recursive comparison of the collections of their immediate subterms. If we consider these collections as unordered multisets, we are dealing with the multiset path order; on the other hand, if we consider the collections as ordered tuples, we have the lexicographic path order. The RPO is nothing more than a combination of both.
Permutation equations are of the form \(f(x_1,\ldots ,x_n) \approx f(x_{\pi (1)},\ldots ,x_{\pi (n)})\), where \(\pi \) is a permutation on \(\{1,\ldots ,n\}\) and \(f\) is a \(n\)-ary symbol [1]. Commutativity can be expressed using the permutation equation \(f^C(x,y)\approx f^C(y,x)\), where \(f^C\) is a binary symbol. This equation cannot be oriented into a rewrite rule without losing termination of the entire system, which means the equation cannot be oriented by well-founded orderings. In order to circumvent this problem, a first-order version of the RPO working modulo permutation equations was given in [6]. The proposal was to use a reduction order \(\succ _E\), for a set of permutation equations \(E\), that is \(E\)-compatible and is useful for the termination of a rewriting system modulo \(E\). We would like to do something similar, but for the nominal framework and considering only the commutativity as a permutation equation.
The nominal framework [5] has become a promising method for dealing with languages involving binders such as the lambda calculus and first-order logic. Within this framework, \(\alpha \)-equivalence (denoted as \(\approx _{\alpha }\)) is used instead of syntactic equality, and freshness constraints are directly integrated within the nominal reasoning rather than being left to be handled by the meta-language. We then use expressions like \(a\#X\) ("\(a\) is fresh for \(X\)") to say that the name \(a\) does not belong in the set of free variables of instances of the variable \(X\). In other words, if \(a\) occurs in instances of \(X\) it must be abstracted by some binder, similarly to \(\lambda \) in the lambda calculus, or \(\exists ,\forall \)-quantification in first-order logic. Note that \(a\) and \(X\) are variables at different levels: \(X\) is a meta-level variable that represents an entire expression and can be instantiated, but not bound by abstractions; whereas \(a\) is an object-level variable, called atom, which can be bound, but not instantiated.
Extending first-order rewriting to work modulo both \(\alpha \)-equivalences and commutative axioms has its difficulties. First we need to distinguish the set of oriented equations - the set of rewrite rules \(R\) - and the set of unoriented ones - the commutative set \(C\), which consists of a set built by commutative permutation equations. Then we will need two different rewrite relations: nominal \(R/C\)-rewriting applies rules from \(R\) to the equivalence class modulo \(\approx _{\alpha ,C}\) of a nominal term \(t\), while \(R,C\)-rewriting uses nominal \(C\)-matching to determine if a rule in \(R\) applies to a nominal term, say \(t\). This way, we take the commutativity into account without explicitly using it as a rule. The challenge is that the definition of the relations \(R/C\) and \(R,C\) also features freshness conditions, since this nominal term \(t\) may have variables.
In this talk, we will present our work in progress in the development of a reduction order for commutative nominal rewrite systems called \(>_{{\sf Crpo}}\). This ordering brings together the ideas behind orderings dealing with \(\alpha \)-equivalence from [4] and orderings dealing with permutation equations from [6], and in our case we consider specifically the commutative equation. This is a work in progress and we still want to present a completion procedure for commutative nominal rewrite systems in the future.
[1] Jürgen Avenhaus (2004): Efficient Algorithms for Computing Modulo Permutation Theories. In David Basin & Michael Rusinowitch, editors: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, Lecture Notes in Computer Science 3097, Springer, pp. 415-429, doi:10.1007/978-3-540-25984-8_31.
[2] Franz Baader & Tobias Nipkow (1998): Term rewriting and all that. Cambridge University Press.
[3] Nachum Dershowitz (1982): Orderings for term-rewriting systems. Theoretical Computer Science 17(3), pp. 279-301, doi:10.1016/0304-3975(82)90026-3.
[4] Maribel Fernández & Albert Rubio (2012): Nominal Completion for Rewrite Systems with Binders. In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts & Roger Wattenhofer, editors: Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, Lecture Notes in Computer Science 7392, Springer, pp. 201-213, doi:10.1007/978-3-642-31585-5_21.
[5] Murdoch Gabbay & Andrew M. Pitts (2002): A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput. 13(3-5), pp. 341-363, doi:10.1007/s001650200016.
[6] Dohan Kim & Christopher Lynch (2021): An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. In Naoki Kobayashi, editor: 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), LIPIcs 195, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 19:1-19:17, doi:10.4230/LIPICS.FSCD.2021.19.
