# Exploring the Knowledge Problems for Graph Embedded Rewrite Systems

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen

► To cite this version:

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen. Exploring the Knowledge Problems for Graph Embedded Rewrite Systems. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05149051

HAL Id: hal-05149051

https://inria.hal.science/hal-05149051v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Exploring the Knowledge Problems
for Graph Embedded Rewrite Systems

Serdar Erbatur<sup>1</sup>, Andrew M. Marshall<sup>2</sup>, Paliath Narendran<sup>3</sup>, and Christophe Ringeissen<sup>4</sup>

<sup>1</sup> University of Texas at Dallas, Richardson, TX, USA
serdar.erbatur@utdallas.edu

<sup>2</sup> University of Mary Washington, Fredericksburg, VA, USA
marshall@umw.edu

<sup>3</sup> University at Albany, SUNY, Albany, NY, USA
pnarendran@albany.edu

<sup>4</sup> Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
christophe.ringeissen@loria.fr

Abstract

In this paper, we consider the knowledge problems of deduction and static equivalence in the formal analysis of security protocols. These knowledge problems are decidable for the class of subterm convergent rewrite systems, and more generally for a larger class called contracting convergent.

We explore the gap between the contracting convergent rewrite systems, and a larger superclass called graph-embedded rewrite systems for which the knowledge problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the knowledge problems. We show that several ways of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph embedded rules is still sufficient to obtain undecidability.

Moreover, we extend a recent result that developed decision procedures for the knowledge problems in any subterm rewrite system which is convergent modulo a restricted form of permutative theory. Here, we replace the subterm rewrite system with a contracting one. We show that the previous result can be extended to obtain decision procedures for contracting rewrite systems modulo some permutative theories.

# 1 Introduction

The class of subterm rewrite systems (TRSs) is very useful in protocol analysis [1] to specify intruder theories for which the problems of deduction and static equivalence are decidable. In a subterm TRS, any right-hand side is a subterm of its left-hand side. In protocol analysis, there is an obvious need of considering TRSs that are not just subterm ones. In recent work [5, 6], an extension to subterm TRSs, called *graph-embedded TRSs*, was developed. This class of rewrite systems takes advantage of the graph minor relation in term graphs to define a superclass of subterm TRSs. However, for the class of graph-embedded TRSs, the problems of deduction and static equivalence are undecidable. Therefore, in [5, 6], a class of theories called *contracting* is identified, which lies between graph-embedded and subterm TRSs and for which both deduction and static equivalence are decidable.

This paper explores the gap between the contracting and graph-embedded definitions. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of deduction and static equivalence, allowing consideration of a wider class of theories.
We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence.

Furthermore, we explore the possibility of additional restrictions to the graph-embedded definition, considering a subset of the rules forming the definition. We show that this subset of rules is still sufficient to obtain undecidability for deduction and static equivalence. Thus, while it is probable that the gap could be decreased between the two and still maintain decidability, the best approach to achieving this is still an open question.

In addition to these undecidability results, we are also investigating the possibility of extend-
ing the decision procedures developed in [8], which provide decision procedures for deduction
and static equivalence in the theory R ∪ E, where R is a subterm convergent TRS and E a
(restricted type of) permutative theory. We report here on ongoing research to extend this
decidability result by replacing the subterm convergent TRS with a contracting convergent
TRS.

2 Preliminaries

We use the standard notation of equational unification [4] and term rewriting systems [3]. The applied pi calculus and frames are used to model attacker knowledge [2]. In this model, the set of messages or terms which the attacker knows are the set of terms in Ran(σ) of the frame φ = ν̃n.σ, where σ is a substitution ranging over ground terms. ñ consists of a finite set of restricted names, these names represent freshly generated names which remain secret from the attacker. The set of names occurring in a term t is denoted by fn(t). For any frame φ = ν̃n.σ, let fn(φ) be the set of names fn(σ)\̃n where fn(σ) = ⋃t∈Ran(σ) fn(t); and for any term t, let tφ denote by a slight abuse of notation the term tσ. We say that a term t satisfies the name restriction (of φ) if fn(t) ∩ ñ = ∅. The set of subterms occurring in σ is denoted by St(σ).

**Definition 1 (Deduction).** Let $\phi = \nu\tilde{n}.\sigma$ be a frame, and $t$ a ground term. We say that $t$ is deduced from $\phi$ modulo $E$, denoted by $\phi \vdash_E t$, if there exists a term $\zeta$ such that $\zeta\sigma =_E t$ and $fn(\zeta) \cap \tilde{n} = \emptyset$. The term $\zeta$ is called a *recipe of t* in $\phi$ modulo $E$.

Another form of knowledge is the ability to tell if two frames are statically equivalent modulo $E$, sometimes also called *indistinguishability*.

**Definition 2 (Static Equivalence).** Two terms $s$ and $t$ are equal in a frame $\phi = \nu\tilde{n}.\sigma$ modulo an equational theory $E$, denoted ($s =_E t$)$\phi$, if $s\sigma =_E t\sigma$, and $\tilde{n} \cap (fn(s) \cup fn(t)) = \emptyset$. The set of all equalities $s = t$ such that ($s =_E t$)$\phi$ is denoted by $Eq(\phi)$. Given a set of equalities $Eq$, the fact that ($s =_E t$)$\phi$ for any $s = t \in Eq$ is denoted by $\phi \models Eq$. Two frames $\phi = \nu\tilde{n}.\sigma$ and $\psi = \nu\tilde{n}.\tau$ are statically equivalent modulo $E$, denoted as $\phi \approx_E \psi$, if $Dom(\sigma) = Dom(\tau)$, $\phi \models Eq(\psi)$ and $\psi \models Eq(\phi)$.

Let us now introduce the graph-embedded and contracting TRSs.

**Definition 3 (Leaf and Subterm Permutations).** We define two permutations, $\approx_s$ and $\approx_l$:

1. For terms $t$ and $t'$, we say $t$ is subterm permutatively equal to $t'$, denoted $t \approx_s t'$, if one of the following is true:

(a) $t = t'$, where $t$ and $t'$ are constants or variables, or

(b) $t = f(u_1, \dots, u_n)$ and $t' = f(u_{\sigma(1)}, \dots, u_{\sigma(n)})$ where $f$ is a $n$-ary function symbol, $n \ge 1$, and $\sigma$ is a permutation of the indexes $(1, \dots, n)$.
2. For terms $t$ and $t'$, we say $t$ is leaf permutatively equal to $t'$, denoted $t \approx_l t'$, if $t'$ is obtained from $t$ by applying a permutation on the set of leaves (variables and constants) occurring in $t$.

We will use a combination of the above two permutations in the definition employed for graph-embedded TRS.

**Definition 4 (Permutatively Equal).** For terms $t$ and $t'$, we say $t$ is permutatively equal to $t'$, denoted $t \approx t'$, if $t \approx_s t'' \approx_l t'$, for some term $t''$.

The class of contracting TRS first starts by modeling the graph minor relation in the TRS setting. This is done by a set of rewrite schemas. This set of rewrite schemata then induces a graph-embedded term rewrite system.

**Definition 5 (Graph Embedding).** Consider the following reduction relation, $\rightarrow_{R_{gemb}}^*$, where $R_{gemb}$ is the set of rules given by the instantiation of the following rule schema:

$$ \left\{ \begin{array}{l} \text{for any } f \in \Sigma \\ (1) \quad f(x_1, \dots, x_n) \rightarrow x_i \\ (2) \quad f(x_1, \dots, x_{i-1}, x_i, x_{i+1}, \dots, x_n) \rightarrow f(x_1, \dots, x_{i-1}, x_{i+1}, \dots, x_n) \\ \text{and for any } f, g \in \Sigma \\ (3) \quad f(x_1, \dots, x_{i-1}, g(\tilde{z}), x_{i+1}, \dots, x_m) \rightarrow g(x_1, \dots, x_{i-1}, \tilde{z}, x_{i+1}, \dots, x_m) \\ (4) \quad f(x_1, \dots, x_{i-1}, g(\tilde{z}), x_{i+1}, \dots, x_m) \rightarrow f(x_1, \dots, x_{i-1}, \tilde{z}, x_{i+1}, \dots, x_m) \end{array} \right\} $$

We say a term $t'$ is graph-embedded in a term $t$, denoted $t \succcurlyeq_{gemb} t'$, if $t'$ is a well-formed term such that $t \rightarrow_{R_{gemb}}^* t'$. A TRS $R$ is graph-embedded if for any $l \rightarrow r \in R$, $l \succcurlyeq_{gemb} r$ or $r$ is a constant.

**Remark 1.** Notice that the rules in $R_{gemb}$ ignore function arity, thus intermediate terms between $t$ and $t'$ may not be well-formed. It is only the final term which must be well-formed. Notice also that the schemata are being used to establish the graph-embedded property of a TRS and that can be done without having to construct all of $R_{gemb}$.

**Example 1.** Consider the rule unblind(sign(blind(x, y), z), y) $\rightarrow$ sign(x, z) from the theory of blind signatures. This rule (and the entire theory) is graph-embedded. Let's consider the derivation for this rule. First, unblind(sign(blind(x, y), z), y) $\rightarrow_{(1)}$ sign(blind(x, y), z). Then, sign(blind(x, y), z) $\rightarrow_{(4)}$ sign(x, y, z). Notice again that this intermediate term is not well-formed. Finally, sign(x, y, z) $\rightarrow_{(2)}$ sign(x, z) $\approx$ sign(x, z).

The graph-embedded class is not sufficient to obtain decidability of static equivalence, so we next need to introduce a type of projection rule that ensures access to subterms and thus decidability of static equivalence.

**Definition 6 (Projecting Rule).** Let $R$ be a TRS, $x$ a variable and $t$ a term with a single occurrence of $x$. A projecting rule in $R$ over $t$ leading to $x$ is a rule in $R$ which is a variant of $t' \rightarrow x$ where $t'$ is a superterm of $t$ with no additional occurrences of $x$.

How these projecting rules relate to the entire term-rewrite system can now be defined.

**Definition 7 (Projection-Closed Derivation).** Let $R$ be a TRS. A non-empty $R_{gemb}$-derivation is said to be projection-closed with respect to $R$ if it has the form $s \rightarrow_{R_{gemb}}^{l \rightarrow r, \gamma} s' \rightarrow_{R_{gemb}}^*$ $t$, where $s$ is a linear term and $t$ is a well-formed term, $l \rightarrow r$ is a $R_{gemb}$ rule among (1), (2) and (4),
$\gamma$ is a substitution ranging over variables. If $l \to r$ is rule (1), then for any $x_i\gamma$ occurring in $t$ there exists a projecting rule in $R$ over $f(x_1, \dots, x_n)\gamma$ leading to $x_i\gamma$. If $l \to r$ is rule (4), then for any $z_i\gamma$ occurring in $t$ there exists a projecting rule in $R$ over $g(\bar{z})\gamma$ leading to $z_i\gamma$. Finally, $s' \to_{R_{gemb}}^* t$ is either projection-closed with respect to $R$ or empty.

Notice in the above definition rule (2) of $R_{gemb}$ can be used in a projection-closed derivation, but no projecting rule need to be added when rule (2) is used.

**Definition 8 (Projection-Closed Permutative Equality).** Let $R$ be a TRS and $l = r$ a permutative equality obtained by one or zero applications of $\approx_s$ followed by one or zero applications of $\approx_l$. The equality $l = r$ is said to be projection-closed with respect to $R$ if the following holds: for any variable $x$ occurring in a strict subterm $l' \neq x$ of $l$ and in a strict subterm $r'$ of $r$ such that $l' \neq r'$, then there exists a projecting rule in $R$ over $l'$ leading to $x$.

Based on Definitions 7 and 8, we can now introduce the subset of graph-embedded rules for which we can obtain decidability of the knowledge problems.

**Definition 9 (Contracting TRS).** A TRS $R$ is said to be contracting if for any non-subterm rule $l \to r$ in $R$ one of the following holds:

* there exist a position $p$ of $l$, a substitution $\sigma$ ranging over variables, a projection-closed derivation $g \to_{R_{gemb}}^+ d$ with respect to $R$ such that $l|_p = g\sigma$ and $r = d\sigma$ is of depth 1,

* $l = r$ is a permutative equality of depth 2 which is projection-closed with respect to $R$.

## 3 Undecidability Results

One approach that could be investigated to expand the above results would be to try to weaken the definition of projection closed equality so that more permutative theories could be considered in the framework of contracting TRS.

**Definition 10 (Permutative Contracting).** A TRS is permutative contracting if for any non-subterm rule $l \to r$ in $R$, $l = r$ is a permutative equality of arbitrary depth and projection-closed with respect to $R$.

By weakening Definition 9 to Definition 10 we run into undecidability of static equivalence.

**Lemma 1.** Static equivalence is undecidable in general for permutative contracting TRS.

*Proof.* In [7] it is shown that a Linear Bounded Automaton's (LBA) transition function can be simulated by a leaf permuting theory. This is then used to show that static equivalence is undecidable in leaf permuting theories. However, we need to modify the construction to remove overlaps when projection rules are added. We do this by adding an additional “dummy” state to the LBA simulating permutative rules of the construction. This can be done by increasing the arity of $h$, which encodes states, by one. The second to last position being the left-dummy state and the final position the right dummy-state. Thus if $|Q| = n$, $h$ has arity of $n + 2$. For example, if $|Q| = 2$, then the left-dummy state $q_{ld} = h(a, a, b, a)$ and the right $q_{rd} = h(a, a, a, b)$. Right moves by the LBA change the dummy state, that are now left of the LBA tape head, to left-dummy states. Likewise, left rule moves of the LBA change left-dummy states back to right-dummy states. For example, the right moves are modified as follows:

$$ \begin{aligned} f(h(b, a, a, a), g(b, a, a, a), f(h(a, a, a, b), g(a, a, b, a), x)) &\to \\ f(h(a, a, b, a), g(b, a, a, a), f(h(a, b, a, a), g(a, a, b, a), x)) \end{aligned} $$
A similar modification is mode for the left moves. Now when we add the projection rules for right LBA moves we have rules of the form:

$$f(h(a, a, b, a), g(a, a, b, a), x) \to x$$

Now we avoid the rule overlap. The resulting system still simulates the LBA but is now contracting convergent. □

Thus, while the above restrictions detailed in Definition 9 may be able to be weakened slightly, one still requires restrictions on both the rule applications and the permutations. We next show that even if we consider a restricted set of rules from the graph-embedded definition we still have undecidability.

**Definition 11.** A rule-4 graph-embedded, $R_4$, term rewrite system is any TRS, $R$, such that for all $l \to r \in R$, $l \to_{R_{gemb}}^+ r$, using only rules (4) and (2) of Definition 5. Likewise, A rule-3 graph-embedded, $R_3$ term rewrite system is any TRS, $R$, such that for all $l \to r \in R$, $l \to_{R_{gemb}}^+ r$, using only rules (3) and (2) of Definition 5.

First, we consider the rule-4 systems and show that even with these restricted systems we still have undecidability of the knowledge problems.

**Theorem 1.** *Deduction is undecidable in general for rule-4 graph-embedded TRS.*

*Proof.* Assume for each $l \to r \in R$, for some TRS $R$, that $l \to_{R_{gemb}}^* r$, $r$ is homeomorphically embedded in $l$, and the root symbol of $l$ remains the root symbol for $r$. Then, $l \to_{(4)}^* r$. Notice that any homeomorphic rewrite step below the root can be emulated by several applications of rule (4) and (2). If $t = f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{R_{gemb}} f(\bar{t}_1, x_i, \bar{t}_2)$, then $t = f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{(4)} f(\bar{t}_1, x_1, \dots, x_i, \dots, x_n, \bar{t}_2) \to_{(2)} f(\bar{t}_1, x_i, \bar{t}_2)$.

In [5] it is shown that deduction is undecidable in general for homeomorphic embedded TRS. The proof uses a reduction from the Modified Post Correspondence Problem (MPCP). The TRS developed in that reductions was the following:

$$B = \bigcup_{i=1}^{n} \{f(\tilde{\alpha}_i(x), g_i(y), \tilde{\beta}_i(z), \text{unlocked}(z)) \to f(x, y, z, \text{unlocked}(z))\},$$

$$U = \{f(x, y, x, \text{locked}(\text{unlocked}(z))) \to f(x, y, x, \text{unlocked}(z))\}.$$

Notice that each of these rules is both homeomorphic embedded and root symbol preserving. Thus, each of these rules is also rule-4 graph-embedded. □

Next, consider the rule-3 graph-embedded TRSs. For this reduction we will use the Modified Post Correspondence Problem (MPCP). Let $\Gamma = \{a, b\}$ be the alphabet of the MPCP problem. An instance of the problem is a finite set of string pairs, $S = \{(\alpha_i, \beta_i) | i \in [1, n]\} \subseteq \Gamma^+ \times \Gamma^+$, and an input string $\alpha_0 \in \Gamma^*$. A solution is a sequence of indexes $i_1, \dots, i_k \in [1, n]$ such that $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$, $\alpha_0$ is a suffix of $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k}$, and of $\beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$.

**Theorem 2.** *Deduction is undecidable in general for rule-3 graph-embedded TRS.*

*Proof.* Let $f$ be a binary function symbol, $a, b, d, d_0, d_1, \dots, d_n$, be public constants. For $\gamma \in \Gamma^+$ and $x \in V$, let $\gamma(x)$ denote the term version of the string $\gamma$ as follows: If $\gamma = a$ then $\gamma(x) = f(a, x)$. If $\gamma = a \cdot \gamma'$ then $\gamma(x) = f(a, \gamma'(x))$. Let $lck$, $ulck$, and $d$ be public constants. Now, construct a rule-3 TRS, $R$, as follows: for each pair $\{(\alpha_i, \beta_i) | i \in [1, n]\}$ we create the rule

$$f(f(f(ulck, v), f(d_i, x)), f(\tilde{\alpha}_i(y), \tilde{\beta}_i(z))) \to f(f(f(ulck, v), x), f(y, z)).$$
Add one final “locking” rule to R :

$$
f(f(f(ulck, f(lck, v)), f(d_0, x)), f(y, y)) \to f(f(f(ulck, v), x), f(y, y)).
$$

Now for the *MPCP* instance, construct the frame $\phi = \nu\tilde{n} \cdot \sigma$ with $\tilde{n} = \{c, e\}$ and $\sigma = \{v \mapsto f(ulck, f(lck, e)), x \mapsto \tilde{\alpha}_0(c)\}$. Finally, the deduction problem is given by $\phi$ and the term $M = f(f(ulck, e), d), f(c, c))$. $\square$

4 Equational Rewriting Modulo Permutative Theories

In this section we briefly review some ongoing work investigating decision procedures for the
knowledge problems in the combined theory R ∪ E, where E is a permutative theory and
R is E-convergent. The investigated approach relies on the possibility of computing a finite
representation of all the terms that are matched modulo E by the left-hand sides of the TRS R.

**Definition 12.** An *E*-variant of a term *l* is a pair (*t*, *σ*) such that *t* =<sub>*E*</sub> *lσ* and the domain of *σ* is included in the set of variables of *l*. Given two *E*-variants (*u*, *θ*) and (*v*, *γ*) of a term *l*, (*u*, *θ*) is more general than (*v*, *γ*), denoted by (*u*, *θ*) ≤<sub>*E*</sub> (*v*, *γ*) if there exists a substitution *τ* such that *uτ* =<sub>*E*</sub> *v* and *θτ* =<sub>*E*</sub> *γ*. A complete set of *E*-variants of *l*, denoted by *CV*<sub>*E*</sub>(*l*), is a set of *E*-variants of *l* such that for any *E*-variant (*v*, *γ*) of *l*, there exists (*u*, *θ*) ∈ *CV*<sub>*E*</sub>(*l*) such that (*u*, *θ*) ≤<sub>*E*</sub> (*v*, *γ*). The equational theory *E* is said to have the Finite Equational Variant Property (FEVP, for short) if any term admits a finite complete set of *E*-variants.

In [8], we have developed a general procedure that, when terminating, computes a finite set of terms E-matched by *l*, denoted by *CMT*<sub>*E*</sub>(*l*) and such that {(*t*, *σ*) | *t* ∈ *CMT*<sub>*E*</sub>(*l*), *lσ* =<sub>*E*</sub> *t*} is a finite *CV*<sub>*E*</sub>(*l*). This procedure is guaranteed to terminate for permutative theories closed under paramodulation, and so any permutative theory closed by paramodulation has the FEVP.

Under the assumption that *R* is a TRS where for any *l* → *r* ∈ *R*, *CMT*<sub>*E*</sub>(*l*) is finite, the size of *R* modulo *E*, denoted by |*R*|, is defined as follows: |*R*| = max{|*t*| | *t* ∈ *CMT*<sub>*E*</sub>(*l*), *l* → *r* ∈ *R*}. Using the same reduction lemmas as the ones initially developed in [8] for subterm *E*-convergent TRSs, we get the following result for contracting *E*-convergent TRSs.

**Theorem 3.** Let $RE = R \cup E$ where $E$ is any permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. If both deduction and static equivalence are decidable in $E$, then both deduction and static equivalence are decidable in $RE$.

References

[1] Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. *Theor. Comput. Sci.*, 367(1-2):2–32, 2006.

[2] Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Chris Hankin and Dave Schmidt, editors, *Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, London, UK, January 17-19, 2001, pages 104–115. ACM, 2001.

[3] Franz Baader and Tobias Nipkow. *Term rewriting and all that*. Cambridge University Press, New York, NY, USA, 1998.

[4] Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning*, pages 445–532. Elsevier and MIT Press, 2001.
[5] Carter Bunch, Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge problems in protocol analysis: Extending the notion of subterm convergent, 2025. URL: https://arxiv.org/abs/2401.17226, arXiv:2401.17226.

[6] Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories. In Marco Gaboardi and Femke van Raamsdonk, editors, *8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)*, volume 260 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 30:1–30:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.30, doi:10.4230/LIPIcs.FSCD.2023.30.

[7] Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Deciding knowledge problems modulo classes of permutative theories. In Juliana Bowles and Harald Søndergaard, editors, *Logic-Based Program Synthesis and Transformation - 34th International Symposium, LOPSTR 2024, Milan, Italy, September 9-10, 2024, Proceedings*, volume 14919 of *Lecture Notes in Computer Science*, pages 47–63. Springer, 2024. doi:10.1007/978-3-031-71294-4\_3.

[8] Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Computing knowledge in equational extensions of subterm convergent theories. *Math. Struct. Comput. Sci.*, 30(6):683–709, 2020.