Implementing Nominal Unification

DOI10.1016/j.entcs.2006.09.027zbMath1278.68118OpenAlexW2102485270MaRDI QIDQ2867897

Maribel Fernández, Christophe Calvès

Publication date: 20 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.09.027

zbMATH Keywords

unificationnominal syntaxtermgraphs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Nominal Matching and Alpha-Equivalence ⋮ A polynomial nominal unification algorithm ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ Nominal Unification from a Higher-Order Perspective

Uses Software

• Maude
• OCaml

Cites Work

• Nominal unification
• Unification of higher-order patterns in linear time and space
• Numbering matters
• Logic Programming

This page was built for publication: Implementing Nominal Unification