Terminating non-disjoint combined unification
From MaRDI portal
Publication:2119106
DOI10.1007/978-3-030-68446-4_6OpenAlexW3130743698MaRDI QIDQ2119106
Andrew M. Marshall, Christophe Ringeissen, Serdar Erbatur
Publication date: 23 March 2022
Full work available at URL: https://hal.inria.fr/hal-02967029
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computing knowledge in security protocols under convergent equational theories
- Unification in a combination of arbitrary disjoint equational theories
- Deciding knowledge in security protocols under equational theories
- Unification problems with one-sided distributivity
- Unification in combinations of collapse-free regular theories
- Syntacticness, cycle-syntacticness and shallow theories
- Unification in the union of disjoint equational theories: Combining decision procedures
- Folding variant narrowing and optimal variant termination
- Reviving basic narrowing modulo
- Rule-based unification in combined theories and the finite variant property
- Notions of knowledge in combinations of theories sharing constructors
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- On Forward Closure and the Finite Variant Property
- On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Completion of a Set of Rules Modulo a Set of Equations
- Variant-Based Satisfiability in Initial Algebras
- Term Rewriting and All That
- Hierarchical Combination
- Computing knowledge in equational extensions of subterm convergent theories
- Term Rewriting and Applications
This page was built for publication: Terminating non-disjoint combined unification
