Pith. sign in

REVIEW 4 major objections 4 minor 53 references

Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Nominal narrowing, extended with a freshness-aware coherence condition, gives a complete search procedure for unification in languages with binders and equational axioms.

desk verdict The paper's headline E-Lifting Theorem is stated too strong—the converse direction fails without a normalised-substitution hypothesis that Lemma 3 already requires—but the underlying framework and the later completeness results are worth engaging. read the letter →

arxiv 2505.14895 v1 pith:UUOGTCQ4 submitted 2025-05-20 cs.LO

Maribel Fernández , Daniele Nantes-Sobrinho , Daniella Santaguida This is my paper · ORCID
classification cs.LO MSC 68Q4203B70
keywords nominalrewritingnarrowingequationalunificationfreshnessconstraintsalpha-equivalenceE-coherenceliftingtheorembasic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that solving equations in languages with binders—where terms are identified up to renaming of bound names, freshness of variables, and equational axioms such as commutativity—can be reduced to a search procedure called narrowing. The key step is a new property, nominal E-coherence for terms-in-context, which guarantees that rewriting modulo an equational theory E and rewriting with E-matching produce the same normal forms. With that property, the paper proves a lifting theorem: every finite rewriting sequence corresponds to a finite narrowing sequence, and vice versa. It then uses closed narrowing to build a sound and complete unification procedure for theories $T=R\cup E_\alpha$, and refines it with basic narrowing to obtain termination in the pure $\alpha$ case. The payoff is a uniform way to reason about binders, freshness, and structural congruences in applications such as symbolic differentiation.

What carries the argument

The central object is the pair of rewriting relations defined on nominal terms-in-context: $\to_{R/E}$, which rewrites inside an $(\alpha \cup E)$-equivalence class, and $\to_{R,E}$, which uses E-matching directly on a representative. The load-bearing property is nominal E-coherence under freshness conditions: whenever two terms are E-equal and one takes an $R,E$-step, the other can take an $R,E$-step so that the results are again E-equal. Theorem 1 shows this property is equivalent to equality of normal forms of the two relations, and Theorem 2 then lifts every rewriting derivation to a narrowing derivation by replacing matching with unification. The closed variant adds a freshness side condition involving fresh atoms and variables, which is what makes the completeness argument for unification go through.

What would settle it

Run the closed narrowing procedure on the symbolic-differentiation unification problem of Section 5.2, and on variants that include a fixed-point equation such as $(a\,b)\cdot X \approx_C X$. A T-unifiable instance that produces no narrowing derivation ending in an E-solvable pair would refute the completeness theorem; a pair of terms with the same $R/E$-normal form but different $R,E$-normal forms would refute coherence for that system.

Watch

Extended reading notes

Core claim

The paper's central claim is that rewriting and narrowing can be made to correspond exactly in the nominal setting, modulo $\alpha$-equivalence and an equational theory $E$, provided a freshness-aware condition called nominal E-coherence holds. Under that condition, together with E-convergence of the rewrite system and an existing complete E-unification algorithm, the E-lifting theorem matches every finite $R,E$-rewriting sequence with a finite $E$-narrowing sequence, and the closed narrowing theorem shows that derivations ending in an E-solvable pair form a complete set of $T$-unifiers for closed well-structured $T=R\cup E_\alpha$. A unification problem is thereby solved by narrowing a pair of terms in parallel until they become E-equal, without inspecting entire $(\alpha\cup E)$-equivalence classes. The paper additionally proves that for $E=\emptyset$, closed basic narrowing remains complete and terminates under a guarantee that basic derivations from right-hand sides terminate.

Load-bearing premise

The load-bearing premise is that the relation $\to_{R,E}$ is E-coherent for the theory at hand, a universal condition that the paper gives no procedure for checking; if it fails, the lifting and completeness theorems no longer follow.

Editorial extensions

If this is right

  • For any closed well-structured $T=R\cup E_\alpha$ with E-coherent $\to_{R,E}$, the set of pairs built from closed narrowing derivations that end in an E-solvable pair is a complete set of $T$-unifiers, so a fair search over the narrowing tree solves the unification problem.
  • The E-lifting theorem transfers correctness properties between rewriting and narrowing, so confluence and termination results for $\to_{R,E}$ can be reused to justify unification algorithms rather than re-proving them.
  • When $E=\emptyset$, closed basic narrowing is complete and terminates whenever all basic derivations from right-hand sides terminate, giving a finite complete unification algorithm for convergent closed nominal rewrite systems.
  • For the commutativity theory $C$, the framework yields a nominal $C$-unification procedure, illustrated by symbolic differentiation modulo commutativity in Section 5.2.
  • If $E$ is infinitary, the narrowing tree may be infinite in both width and depth, but because each level is enumerable a fair enumeration still gives a sound and complete procedure.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A syntactic or decidable criterion for E-coherence would substantially widen the framework's applicability, since the paper offers no way to establish it other than checking the definition directly.
  • Example 14 suggests that static positions are the wrong invariant for AC-style axioms; a dynamic, representative-independent notion of position may be the natural repair and would likely also benefit first-order narrowing modulo AC.
  • The fixed-point equations $\pi\cdot X \approx_C X$ that make nominal C-unification non-finitary are a structural feature, not a narrowing artefact; representing fixed-point solutions explicitly could restore finite branching and make theories like C amenable to practical search.
  • Once nominal E-unification algorithms for A and AC are available and E-coherence is checked, the same theorems would immediately supply unification procedures for those theories; the lifting argument itself is not the bottleneck.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper develops a nominal rewriting and narrowing framework modulo an equational theory E, with α-equivalence and freshness built in. It defines two rewriting relations, →R/E and →R,E, introduces a novelty called nominal E-coherence, proves a coherence theorem (Theorem 1), an E-lifting theorem connecting rewriting and narrowing (Theorem 2), and uses closed narrowing to derive a soundness and completeness result for nominal R∪Eα-unification (Theorem 4). The final section adapts basic narrowing for the E=∅ case and discusses why Hullot's property fails for theories like AC. The paper is clearly motivated by applications to languages with binders, and the examples (prenex normal form, symbolic differentiation) illustrate the intended use.

Significance. If the technical claims were correct and adequately supported, this would be a useful general framework: it extends first-order rewriting modulo equational theories to nominal syntax, and it gives a unification procedure for theories decomposable as R∪Eα. The definition of nominal E-coherence under freshness contexts is a genuine contribution, as is the closed-narrowing refinement for E=∅. The paper also honestly flags its main limitations: E-coherence must be checked for each theory, and nominal E-unification algorithms are currently available only for very restricted theories such as C and AC, with C-unification already infinitary. However, the central lifting theorem is false as stated, and the proof of the key completeness lemma contains an unstated construction and a missing normalisation argument. These issues affect the main claimed correspondence between rewriting and narrowing, so the contribution is not yet in a publishable form.

major comments (4)
  1. [§4.1, Theorem 2] Theorem 2 is false as stated because it omits the normalised-substitution hypothesis that Lemma 3 requires. Let E=∅, R={∅⊢f(X)→X}, s0=X, and ρ0=[X↦g(f(a))]. Then R∪Eα is well-structured and →R,E is E-coherent, and the one-step rewriting sequence g(f(a))→R,E g(a) is an instance s0ρ0→R,E g(a). Any R,E-narrowing derivation from s0 must start by solving X ?≈? f(Y), yielding θ=[X↦f(Y)] and s1=Y. For the lifting condition Δ⊢ρ0|V≈Eθρn|V with V={X}, we would need f(Yρn)≈α g(f(a)), which is impossible. Thus no finite narrowing sequence corresponds to this rewriting step. The theorem needs the explicit hypothesis that ρ0 is R,E-normalised, or a restriction to redexes at non-variable positions of s0, and Theorem 3 requires the corresponding correction.
  2. [§4.1, Lemma 3] The proof of the base case asserts 'from hypothesis, ρ0 = θ0ρ1', but no such hypothesis or definition of ρ1 appears in the statement or proof; ρ1 is introduced only at that point. The proof must construct ρ1 explicitly, for example as a suitable restriction of the substitution ρ′ obtained from the completeness of E-unification, and then verify Δ⊢Δ1ρ1, dom(ρ1)⊆V1, and s1ρ1≈E t1. More importantly, the induction step applies the induction hypothesis to the derivation starting from t1 with s1ρ1, which requires ρ1 to be R,E-normalised; the proof never argues that the constructed ρ1 is normalised. Without this, Lemma 3 — and with it the completeness part of Theorem 4 through Lemma 5 — is not established.
  3. [§5.1, Lemma 5 and Theorem 4] Lemma 5's proof appeals to 'the least E-unifier (Γ,µ)' and concludes (Γ,µ)≤E(∆′,ρ). For theories such as C, E-unification is infinitary and a least, most general unifier need not exist. What the argument needs is the defining property of a complete set of E-unifiers: since (∆′,ρ) is an E-solution of {sn≈Etn}, there is some (Γ,µ) in the chosen complete set with (Γ,µ)≤E(∆′,ρ). The wording should be corrected, and Theorem 4 should be formulated relative to the chosen complete sets of E-solutions rather than to a single least unifier.
  4. [§3, Definition 4 and §5.2] E-coherence is the operative hypothesis of Theorems 1, 2, and 4, but the manuscript gives no criterion for it beyond the definition and never verifies it for the running examples. In §5.2 the system Rsub∪Rdiff∪C is asserted to be 'closed and C-convergent', which is not sufficient to apply Theorem 4; the C-coherence of →R,C must be checked separately. Since every application of the completeness theorem depends on this condition, the paper should either prove coherence for the C-example or state clearly that the example is only an illustration of the narrowing relation and not of the completeness theorem.
minor comments (4)
  1. [§3, Definition 4] The definition quantifies over Δ and then ends with 'for some Δ', which is redundant and ill-formed; delete the trailing phrase.
  2. [§5.1, Lemma 5] The notation σ↓ is used for the normal form of a substitution, but a definition of a normal form for a substitution as a syntactic object is not given; define it explicitly.
  3. [§4.1, Theorem 2] The phrase 'and vice versa' conflates two different statements with different hypotheses; state the rewriting-to-narrowing direction and the narrowing-to-rewriting direction separately, each with its own conditions.
  4. [Example 12] The displayed substitutions for θ2 and θn use the term (a⊕b)⊕(b⊕a), whereas Example 4's fixed-point solutions use (a⊕b)⊕(a⊕b); align the notation to avoid confusing the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central lifting and completeness theorems are proved from independently stated hypotheses rather than reduced to their conclusions.

full rationale

The derivation chain is self-contained. Nominal E-coherence (Definition 4) is an independently formulated property of the rewrite relation, not a restatement of the normal-form equivalence it characterizes; Theorem 1 proves an iff from confluence, termination, and coherence, and its forward direction is actually proved rather than assumed. The E-Lifting Theorem is established through Lemma 2 and the converse Lemma 3, which use the explicit hypotheses of well-structuredness and E-coherence to construct narrowing derivations from rewriting derivations; those hypotheses are not the target result in disguise. The unification completeness result (Theorem 4) follows from the separately proved Soundness (Lemma 4) and Completeness (Lemma 5) lemmas, with the availability of a complete E-unification algorithm stated as a premise rather than derived from the theorem. There are no fitted parameters, no empirical predictions, and no known pattern renamed as a new structure. The self-citations [5,9,45] place the work in context and supply prior narrowing machinery, but they are not load-bearing: the paper contains proofs of the main statements rather than deferring them to those citations. The skeptical observation that Theorem 2 as stated omits the R,E-normalised substitution hypothesis required by Lemma 3 is a correctness concern about the literal statement, not a circularity concern, and does not affect the circularity score.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claim rests on four explicitly stated domain assumptions: E-coherence, existence of complete E-unification, E-convergence, and closedness. These are not fitted or invented, but for many theories they are unverified or known to fail.

assumptions (5)
  • domain assumption →R,E is E-coherent (Definition 4).
    Assumed in Theorems 1-4; no general criterion for establishing it is given beyond the definition.
  • domain assumption A complete algorithm for nominal E-unification exists.
    Remark 2 and Theorem 4 require this; currently only C and AC are available, and C-unification is infinitary.
  • domain assumption R is E-convergent (E-terminating and E-confluent).
    Required by the well-structured hypothesis in Remark 2 and used in the proof of the lifting theorem.
  • domain assumption T = R ∪ Eα is closed.
    Definitions 5-6 and Theorem 4 use closedness; it is used for the closed variants of rewriting and narrowing.
  • standard math Standard nominal syntax and metatheory.
    α-equivalence, freshness derivability, matching properties, and the permutation action are used throughout as background.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders." pith.science (2026). https://pith.science/paper/UUOGTCQ4

@misc{pith2026250514895,
  author       = {Pith},
  title        = {Pith review of: Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UUOGTCQ4}},
  note         = {Machine review of arXiv:2505.14895}
}
read the original abstract

Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges arise in the presence of binders, freshness conditions and equational axioms such as commutativity. This is problematic for applications in programming languages and theorem proving, where reasoning modulo renaming of bound variables, structural congruence, and freshness conditions is needed. To address these issues, we present a framework for nominal rewriting and narrowing modulo equational theories that intrinsically incorporates renaming and freshness conditions. We define and prove a key property called nominal E-coherence under freshness conditions, which characterises normal forms of nominal terms modulo renaming and equational axioms. Building on this, we establish the nominal E-lifting theorem, linking rewriting and narrowing sequences in the nominal setting. This foundational result enables the development of a nominal unification procedure based on equational narrowing, for which we provide a correctness proof. We illustrate the effectiveness of our approach with examples including symbolic differentiation and simplification of first-order formulas.

Figures

Figures reproduced from arXiv: 2505.14895 by the authors.

Figure 1
Figure 1. This work: nominal rewriting modulo theories [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Rules for # and ≈α composition of two substitutions θ1 and θ2 is denoted by simple juxtaposition as θ1θ2 and tθ1θ2 = (tθ1)θ2. 2.2. Nominal Constraints and Judgements In the nominal framework, there are two kinds of constraints: (i) s ≈α t is an (alpha-)equality constraint, which means that s and t are equal up to the renaming of bound names; (ii) a#t is a freshness constraint which means that a cannot occur unabstra… view at source ↗
Figure 2
Figure 2. For example, for ∆ = {a#X, b#Z}, θ = [X 7→ f(a, a), Z 7→ c] and ∆θ = {a#f(a, a), b#c} there exists no Γ such that Γ ⊢ a#f(a, a). Thus, ⟨∆θ⟩nf does not exist. Differently, for θ ′ = [X 7→ f(b, Y ), Z 7→ c], we have ⟨∆θ ′ ⟩nf = {a#Y }. A term-in-context ∆ ⊢ t expresses that the term t has the freshness constraints imposed by ∆. For example, a#X ⊢ f(X, h(b)) expresses that a cannot occur free in instances of X. 2.3. Eq… view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: Infinitely branching tree Example 12 (Cont. Example 4). Consider the signature Σ = {h : 1, f C : 2, ⊕ : 2}, where f C and ⊕ are commutative symbols. Let R = { ⊢ h(Y ) → Y, ⊢ f C ([a][b] · Z, Z) → f C (h(Z), h(Z))} be a set of rewrite5 rules. Let ⊢ h(f C ([b][a]X, X)) b…
Figure 4
Figure 4. Figure 4: Corresponding Narrowing to Rewriting Derivations [PITH_FULL_IMAGE:figures/full_fig_p025_4.png]
Figure 5
Figure 5. Figure 5: Rdiff – Rules for Symbolic Differentiation Modulo Commutativity If E is finitary, the narrowing tree for (∆ ⊢ s) ? T ≈? (∇ ⊢ t) is finitely branching (even if it might be infinite in depth), and we can enumerate all the nodes using a standard breadth-first-search strat…
Figure 6
Figure 6. Figure 6: T -unification narrowing tree for the nominal C-unification problem using Rdiff The commutativity of plus is used before instantiating the subterm with the narrowing substitution. Since the initial problem contains the constraint y#G, we can narrow, using rule y#F ⊢ di…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 44 canonical work pages

  1. [1]

    Termination of narrowing revisited

    Alpuente, M., Escobar, S., Iborra, J., 2009. Termination of narrowing revisited. Theoretical Computer Science 410, 4608–4625. doi: https: //doi.org/10.1016/j.tcs.2009.07.037. abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi

    work page doi:10.1016/j.tcs.2009.07.037 2009

  2. [2]

    A needed narrowing strategy

    Antoy, S., Echahed, R., Hanus, M., 2000. A needed narrowing strategy. J. ACM 47, 776–822. doi: 10.1145/347476.347484

    arXiv 2000

  3. [3]

    A formalisation of nominal α- equivalence with A, C, and AC function symbols

    Ayala-Rinc´ on, M., de Carvalho Segundo, W., Fern´ andez, M., Nantes- Sobrinho, D., Oliveira, A.C.R., 2019. A formalisation of nominal α- equivalence with A, C, and AC function symbols. Theor. Comput. Sci. 781, 3–23. doi: 10.1016/j.tcs.2019.02.020

    work page doi:10.1016/j.tcs.2019.02.020 2019

  4. [4]

    Formalising nominal C-unification gener- alised with protected variables

    Ayala-Rinc´ on, M., de Carvalho Segundo, W., Fern´ andez, M., Silva, G.F., Nantes-Sobrinho, D., 2021. Formalising nominal C-unification gener- alised with protected variables. Math. Struct. Comput. Sci. 31, 286–311. doi:10.1017/S0960129521000050

    work page doi:10.1017/s0960129521000050 2021

  5. [5]

    Nominal narrowing, in: Kesner, D., Pientka, B

    Ayala-Rinc´ on, M., Fern´ andez, M., Nantes-Sobrinho, D., 2016. Nominal narrowing, in: Kesner, D., Pientka, B. (Eds.), 1st International Confer- ence on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik. pp. 11:1–11:17. doi:10.4230/LIPIcs.FSCD.2016.11

    work page doi:10.4230/lipics.fscd.2016.11 2016

  6. [6]

    On nom- inal syntax and permutation fixed points

    Ayala-Rinc´ on, M., Fern´ andez, M., Nantes-Sobrinho, D., 2020. On nom- inal syntax and permutation fixed points. Logical methods in computer science 16, 19:1–19:36. doi: 10.23638/LMCS-16(1:19)2020

    work page doi:10.23638/lmcs-16(1:19)2020 2020

  7. [7]

    Nominal AC-matching, in: Dubois, C., Kerber, M

    Ayala-Rinc´ on, M., Fern´ andez, M., Silva, G.F., Kutsia, T., Nantes- Sobrinho, D., 2023. Nominal AC-matching, in: Dubois, C., Kerber, M. (Eds.), Intelligent Computer Mathematics - 16th International Con- ference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings, Springer. pp. 53–68. doi: 10.1007/978-3-031-42753-4\_4

    work page doi:10.1007/978-3-031-42753-4 2023

  8. [8]

    Certified first-order ac-unification and applications

    Ayala-Rinc´ on, M., Fern´ andez, M., Silva, G.F., Kutsia, T., Nantes- Sobrinho, D., 2024. Certified first-order ac-unification and applications. J. Autom. Reason. 68, 25. doi: 10.1007/S10817-024-09714-5 . 41

    work page doi:10.1007/s10817-024-09714-5 2024

Show all 53 references
  1. [9]

    Nominal equational rewriting and narrowing, in: Pre- proceedings of the 19th Logical and Semantic Frameworks with Appli- cations (LSF A 2024), pp

    Ayala-Rinc´ on, M., Fernandez, M., Nantes-Sobrinho, D., de Souza, D.S.M., 2024. Nominal equational rewriting and narrowing, in: Pre- proceedings of the 19th Logical and Semantic Frameworks with Appli- cations (LSF A 2024), pp. 75–93. Available at:https://sites.google. com/ufg....

    2024

  2. [10]

    Term rewriting and all that

    Baader, F., Nipkow, T., 1998. Term rewriting and all that. Cambridge University Press

    1998

  3. [11]

    Tamarin: Verifi- cation of large-scale, real-world, cryptographic protocols

    Basin, D.A., Cremers, C., Dreier, J., Sasse, R., 2022. Tamarin: Verifi- cation of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20, 24–32. doi: 10.1109/MSEC.2022.3154689

    2022

  4. [12]

    Matching and alpha-equivalence check for nominal terms

    Calv` es, C., Fern´ andez, M., 2010. Matching and alpha-equivalence check for nominal terms. J. Comput. Syst. Sci. 76, 283–301. doi: 10.1016/J. JCSS.2009.10.003

    2010 doi

  5. [13]

    The locally nameless representation

    Chargu´ eraud, A., 2012. The locally nameless representation. J. Autom. Reason. 49, 363–408. URL: https://doi.org/10.1007/ s10817-011-9225-2 , doi:10.1007/S10817-011-9225-2

    2012 doi

  6. [14]

    The complexity of equivariant unification, in: D ´ ıaz, J., Karhum¨ aki, J., Lepist¨ o, A., Sannella, D

    Cheney, J., 2004. The complexity of equivariant unification, in: D ´ ıaz, J., Karhum¨ aki, J., Lepist¨ o, A., Sannella, D. (Eds.), Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, Springer. pp. 332–3...

    2004

  7. [15]

    Nominal logic programming

    Cheney, J., Urban, C., 2008. Nominal logic programming. ACM Trans. Program. Lang. Syst. 30. doi: 10.1145/1387673.1387675

    2008

  8. [16]

    Deepsec: Deciding equiv- alence properties for security protocols - improved theory and practice

    Cheval, V., Kremer, S., Rakotonirina, I., 2024. Deepsec: Deciding equiv- alence properties for security protocols - improved theory and practice. TheoretiCS 3. doi: 10.46298/THEORETICS.24.4

    2024 doi

  9. [17]

    Indistinguishability beyond diff- equivalence in proverif, in: 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023, IEEE

    Cheval, V., Rakotonirina, I., 2023. Indistinguishability beyond diff- equivalence in proverif, in: 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023, IEEE. pp. 184–199. doi: 10.1109/CSF57540.2023.00036. 42

    2023

  10. [18]

    The finite variant property: How to get rid of some algebraic properties, in: Giesl, J

    Comon-Lundh, H., Delaune, S., 2005. The finite variant property: How to get rid of some algebraic properties, in: Giesl, J. (Ed.), Term Rewrit- ing and Applications, Springer Berlin Heidelberg, Berlin, Heidelberg. pp. 294–307

    2005

  11. [19]

    Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, in: 18th An- nual IEEE Symposium of Logic in Computer Science, 2003

    Comon-Lundh, H., Shmatikov, V., 2003. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, in: 18th An- nual IEEE Symposium of Logic in Computer Science, 2003. Proceed- ings., pp. 271–280. doi: 10.1109/LICS.2003.1210067

    2003 arXiv

  12. [20]

    Equational programming

    Dershowitz, N., 1988. Equational programming. Oxford University Press, Inc., USA. p. 21–56

    1988

  13. [21]

    Dershowitz, N., Mitra, S., Sivakumar, G., 1992. Decidable matching for convergent systems (preliminary version), in: Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, Springer-Verlag, Berlin, Heidelberg. p. 589–602

    1992

  14. [22]

    Mathematical Logic

    Ebbinghaus, H.D., Flum, J., Thomas, W., 1994. Mathematical Logic. 2 ed., Springer

    1994

  15. [23]

    Variant narrowing and equa- tional unification, in: Rosu, G

    Escobar, S., Meseguer, J., Sasse, R., 2008. Variant narrowing and equa- tional unification, in: Rosu, G. (Ed.), Proceedings of the Seventh In- ternational Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, Elsevier. pp. 103–119. ...

    2008 doi

  16. [24]

    Folding variant narrowing and optimal variant termination

    Escobar, S., Sasse, R., Meseguer, J., 2012. Folding variant narrowing and optimal variant termination. The Journal of Logic and Algebraic Pro- gramming 81, 898–928. doi: https://doi.org/10.1016/j.jlap.2012. 01.002. rewriting Logic and its Applications

    2012 doi

  17. [25]

    Nominal rewriting

    Fern´ andez, M., Gabbay, M., 2007. Nominal rewriting. Inf. Comput. 205, 917–965. doi: 10.1016/j.ic.2006.12.002

    2007 doi

  18. [26]

    Nominal rewriting with name gen- eration: abstraction vs

    Fern´ andez, M., Gabbay, M.J., 2005. Nominal rewriting with name gen- eration: abstraction vs. locality, in: Proceedings of the 7th ACM SIG- PLAN International Conference on Principles and Practice of Declar- ative Programming, Association for Computing Machinery, New York, NY...

    2005

  19. [27]

    Closed nominal rewriting and effi- ciently computable nominal algebra equality, in: Crary, K., Miculan, M

    Fern´ andez, M., Gabbay, M.J., 2010. Closed nominal rewriting and effi- ciently computable nominal algebra equality, in: Crary, K., Miculan, M. (Eds.), Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, ...

    2010 doi

  20. [28]

    A new approach to abstract syntax with variable binding

    Gabbay, M., Pitts, A.M., 2002. A new approach to abstract syntax with variable binding. Formal Aspects Comput. 13, 341–363. doi: 10.1007/ s001650200016

    2002

  21. [29]

    Gabbay, M.J., Mathijssen, A., 2006. One-and-a-halfth-order logic, in: Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, Association for Computing Machinery, New York, NY, USA. p. 189–200. doi: 10.1145/ 1140335.1140359

    2006

  22. [30]

    Higher-order narrowing with definitional trees

    Hanus, M., Prehofer, C., 1999. Higher-order narrowing with definitional trees. J. Funct. Program. 9, 33–75. URL: https://doi.org/10.1017/ s0956796899003330, doi:10.1017/S0956796899003330

    1999 doi

  23. [31]

    Canonical forms and unification, in: Bibel, W., Kowalski, R.A

    Hullot, J., 1980. Canonical forms and unification, in: Bibel, W., Kowalski, R.A. (Eds.), 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, Springer. pp. 318–334. doi:10.1007/3-540-10009-1\_25

    1980 doi

  24. [32]

    Confluent and coherent equational term rewriting systems: Application to proofs in abstract data types, in: Ausiello, G., Protasi, M

    Jouannaud, J., 1983. Confluent and coherent equational term rewriting systems: Application to proofs in abstract data types, in: Ausiello, G., Protasi, M. (Eds.), CAAP’83, Trees in Algebra and Programming, 8th Colloquium, L’Aquila, Italy, March 9-11, 1983, Proceedings, Springe...

    1983 doi

  25. [33]

    Incremental con- struction of unification algorithms in equational theories, in: D ´ ıaz, J

    Jouannaud, J., Kirchner, C., Kirchner, H., 1983. Incremental con- struction of unification algorithms in equational theories, in: D ´ ıaz, J. (Ed.), Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings, Springer. pp. 361–373. do...

    1983 doi

  26. [34]

    Matching, unification and complexity

    Kapur, D., Narendran, P., 1987. Matching, unification and complexity. SIGSAM Bull. 21, 6–9. doi: 10.1145/36330.36332. 44

    1987

  27. [35]

    Confluence and commutation for nom- inal rewriting systems with atom-variables, in: Fern´ andez, M

    Kikuchi, K., Aoto, T., 2020. Confluence and commutation for nom- inal rewriting systems with atom-variables, in: Fern´ andez, M. (Ed.), Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Pro- ceedi...

    2020 doi

  28. [36]

    Nominal unification from a higher-order perspective

    Levy, J., Villaret, M., 2012. Nominal unification from a higher-order perspective. ACM Trans. Comput. Logic 13. doi: 10.1145/2159531. 2159532

    2012 doi

  29. [37]

    Foundations of logic programming

    Lloyd, J.W., 1984. Foundations of logic programming. Springer-Verlag, Berlin, Heidelberg

    1984

  30. [38]

    An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis

    L´ opez-Rueda, R., Escobar, S., Sapi˜ na, J., 2023. An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis. J. Log. Algebraic Methods Program. 135, 100895. doi: 10.1016/J.JLAMP.2023.100895

    2023

  31. [39]

    Reasoning with higher-order abstract syntax in a logical framework

    McDowell, R., Miller, D., 2002. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3, 80–

    2002

  32. [40]

    Symbolic reachability analysis using narrowing and its application to verification of cryptographic proto- cols

    Meseguer, J., Thati, P., 2005. Symbolic reachability analysis using narrowing and its application to verification of cryptographic proto- cols. Electronic Notes in Theoretical Computer Science 117, 153–182. doi:https://doi.org/10.1016/j.entcs.2004.06.024. proceedings of the Fi...

    2005 doi

  33. [41]

    Completeness results for ba- sic narrowing

    Middeldorp, A., Hamoen, E., 1994. Completeness results for ba- sic narrowing. Appl. Algebra Eng. Commun. Comput. 5, 213–253. doi:10.1007/BF01190830

    1994 doi

  34. [42]

    Semantic unification for convergent systems

    Mitra, S., 1994. Semantic unification for convergent systems. Technical Report. University of Illinois at Urbana-Champaign. USA

    1994

  35. [43]

    Basic narrowing revisited

    Nutt, W., R´ ety, P., Smolka, G., 1989. Basic narrowing revisited. J. Symb. Comput. 7, 295–317. doi: 10.1016/S0747-7171(89)80014-8 . 45

    1989 doi

  36. [44]

    Solving Higher-Order Equations: From Logic to Programming

    Prehofer, C., 1998. Solving Higher-Order Equations: From Logic to Programming. Progress in Theoretical Computer Science, Birkh¨ auser Boston

    1998

  37. [45]

    Nominal commu- tative narrowing (work in progress), in: Informal Proceedings of UNIF 2024: The 38th International Workshop on Unifica- tion, pp

    Santaguida, D., Nantes-Sobrinho, D., 2024. Nominal commu- tative narrowing (work in progress), in: Informal Proceedings of UNIF 2024: The 38th International Workshop on Unifica- tion, pp. 35–41. URL: https://lat.inf.tu-dresden.de/unif2024/ informal-proceedings-UNIF2024.pdf

    2024

  38. [46]

    Schmidt-Schauß, M., Kutsia, T., Levy, J., Villaret, M., Kutz, Y.D.K.,

  39. [47]

    Type-level computation using narrowing in Ωmega

    Sheard, T., 2007. Type-level computation using narrowing in Ωmega. Electronic Notes in Theoretical Computer Science 174, 105–128. doi:https://doi.org/10.1016/j.entcs.2006.10.040. proceedings of the Programming Languages meets Program Verification (PLPV 2006)

    2007 doi

  40. [48]

    Shinwell, M.R., Pitts, A.M., Gabbay, M.J., 2003. Freshml: program- ming with binders made simple, in: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, As- sociation for Computing Machinery, New York, NY, USA. p. 263–274. doi:10.1145/944...

    2003

  41. [49]

    A unification algorithm for associative-commutative functions

    Stickel, M.E., 1981. A unification algorithm for associative-commutative functions. J. ACM 28, 423–434. doi: 10.1145/322261.322262

    1981

  42. [50]

    Nominal unification

    Urban, C., Pitts, A.M., Gabbay, M., 2004. Nominal unification. Theor. Comput. Sci. 323, 473–497. doi: 10.1016/j.tcs.2004.06.016

    2004 doi

  43. [51]

    E-unifiability via narrowing, in: Restivo, A., Rocca, S.R.D., Roversi, L

    Viola, E., 2001. E-unifiability via narrowing, in: Restivo, A., Rocca, S.R.D., Roversi, L. (Eds.), Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings, Springer. pp. 426–438. doi: 10.1007/3-540-45446-2\_27 . 46

    2001 doi

  44. [136]

    URL: https://doi.org/10.1145/504077.504080, doi: 10.1145/ 504077.504080

  45. [2022]

    Nominal unification and matching of higher order expressions with recursive let. Fundam. Informaticae 185, 247–283. doi: 10.3233/ FI-222110

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.