Formalising nominal C-unification generalised with protected variables
From MaRDI portal
Publication:5022930
DOI10.1017/S0960129521000050zbMath1495.68109OpenAlexW3160798129MaRDI QIDQ5022930
Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho, Gabriel Ferreira Silva, Washington de Carvalho-Segundo
Publication date: 20 January 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129521000050
Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The theory of idempotent semigroups is of unification type zero
- Complete axiomatizations of some quotient term algebras
- Complexity of unification problems with associative-commutative operators
- Matching and alpha-equivalence check for nominal terms
- Associative-commutative unification
- Unification theory
- Nominal C-unification
- On solving nominal fixpoint equations
- Completeness in PVS of a nominal unification algorithm
- Nominal unification
- Unification in the union of disjoint equational theories: Combining decision procedures
- A formalisation of nominal C-matching through unification with protected variables
- Nominal rewriting
- Nominal unification of higher order expressions with recursive let
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Nominal Sets
- The First-Order Nominal Link
- Matching, unification and complexity
- Fixed-Point Constraints for Nominal Equational Unification
- A Certified Functional Nominal C-Unification Algorithm
- An Efficient Nominal Unification Algorithm
- Rewriting Techniques and Applications
This page was built for publication: Formalising nominal C-unification generalised with protected variables
