Formalising nominal C-unification generalised with protected variables

DOI10.1017/S0960129521000050MaRDI QIDQ5022930zbMATH OpenOpenAlexFDO

Authors Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, G. F. Silva, Daniele Nantes-Sobrinho

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

zbMATH Keywords

C-unificationcommutative theoryCoqformal methodsnominal matchingnominal unificationPVS

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A formalisation of nominal C-matching through unification with protected variables
• A certified functional nominal C-unification algorithm
• Nominal C-unification
• Completeness in PVS of a nominal unification algorithm
• Implementing nominal unification

Cites work

• A certified functional nominal C-unification algorithm
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• A formalisation of nominal C-matching through unification with protected variables
• An efficient nominal unification algorithm
• Associative-commutative unification
• Complete axiomatizations of some quotient term algebras
• 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 and alpha-equivalence check for nominal terms
• Matching, unification and complexity
• Nominal C-unification
• Nominal narrowing
• Nominal rewriting
• 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

(12)

• A formalisation of nominal C-matching through unification with protected variables
• A certified functional nominal C-unification algorithm
• Nominal AC-matching
• Strong nominal semantics for fixed-point constraints
• Nominal anti-unification modulo equational theories
• Equational generalization problems with atom-variables
• Graded quantitative narrowing
• Equational reasoning modulo commutativity in languages with binders
• A nominal approach to equational problems in languages with binders
• Nominal equational rewriting and narrowing
• Certified first-order AC-unification and applications.
• Nominal equational narrowing: rewriting for unification in languages with binders

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formalising nominal C-unification generalised with protected variables

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