Nominal C-unification

DOI10.1007/978-3-319-94460-9_14zbMath1502.68144arXiv1709.05384OpenAlexW2964141923MaRDI QIDQ1671156

Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Daniele Nantes-Sobrinho, Maribel Fernández

Publication date: 6 September 2018

Full work available at URL: https://arxiv.org/abs/1709.05384

Mathematics Subject Classification ID

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

Related Items (7)

Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ On solving nominal disunification constraints ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Formalising nominal C-unification generalised with protected variables

Uses Software

• Coq

This page was built for publication: Nominal C-unification