Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Equivariant Unification
Authors: James Cheney
Date:Apr 2005
Publication Title:Proc. RTA 2005
Publication Type:Conference Paper
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logic programming or term rewriting systems. Previous work on nominal rewriting and logic programming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic's equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. This paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.
Links To Paper
Springer official version
Bibtex format
author = { James Cheney },
title = {Equivariant Unification},
book title = {Proc. RTA 2005},
year = 2005,
month = {Apr},
url = {,7,36;journal,134,2140;linkingpublicationresults,1:105633,1},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh