A formalisation of nominal C-matching through unification with protected variables

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

zbMATH Keywords

formal methodsCoqnominal unificationcommutative theoryC-unificationnominal matching

Mathematics Subject Classification ID

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

• Coq

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