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

DOI10.1016/J.ENTCS.2019.07.004MaRDI QIDQ2333665zbMATH OpenOpenAlexWikidataFDO

Authors Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, 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

C-unificationcommutative theoryCoqformal methodsnominal matchingnominal unification

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formalising nominal C-unification generalised with protected variables
• A certified functional nominal C-unification algorithm
• Nominal C-unification
• Implementing nominal unification
• An efficient nominal unification algorithm

Cites work

• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• An efficient nominal unification algorithm
• Associative-commutative unification
• Completeness in PVS of a nominal unification algorithm
• Complexity of unification problems with associative-commutative operators
• Fixed-point constraints for nominal equational unification
• scientific article; zbMATH DE number 4049047 (Why is no real title available?)
• scientific article; zbMATH DE number 3688778 (Why is no real title available?)
• Matching, unification and complexity
• Nominal C-unification
• Nominal narrowing
• Nominal sets. Names and symmetry in computer science
• Nominal unification
• Nominal unification of higher order expressions with recursive let
• On solving nominal fixpoint equations
• Rewriting Techniques and Applications
• The First-Order Nominal Link
• The theory of idempotent semigroups is of unification type zero
• Unification in the union of disjoint equational theories: Combining decision procedures
• Unification theory
• Unification theory

Cited in

(3)

• Formalising nominal C-unification generalised with protected variables
• Rewriting with generalized nominal unification
• Nominal equational rewriting and narrowing

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A formalisation of nominal C-matching through unification with protected variables

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2333665)