A formalisation of nominal C-matching through unification with protected variables
From MaRDI portal
Publication:2333665
DOI10.1016/j.entcs.2019.07.004zbMath1433.68186OpenAlexW2969292305WikidataQ113317461 ScholiaQ113317461MaRDI QIDQ2333665
Maribel Fernández, Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Daniele Nantes-Sobrinho
Publication date: 13 November 2019
Full work available at URL: https://doi.org/10.1016/j.entcs.2019.07.004
Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Rewriting with generalized nominal unification ⋮ Formalising nominal C-unification generalised with protected variables
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The theory of idempotent semigroups is of unification type zero
- Complexity of unification problems with associative-commutative operators
- Associative-commutative unification
- Unification theory
- Nominal C-unification
- On solving nominal fixpoint equations
- Completeness in PVS of a nominal unification algorithm
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Nominal unification
- Unification in the union of disjoint equational theories: Combining decision procedures
- 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
- An Efficient Nominal Unification Algorithm
- Rewriting Techniques and Applications
This page was built for publication: A formalisation of nominal C-matching through unification with protected variables