Equivariant Unification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationTerm Rewriting and Applications
Subtitle of host publication16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005. Proceedings
EditorsJürgen Giesl
PublisherSpringer Berlin Heidelberg
Pages74-89
Number of pages16
Volume3467
ISBN (Electronic)978-3-540-32033-3
ISBN (Print)978-3-540-25596-3
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3467

Fingerprint Dive into the research topics of 'Equivariant Unification'. Together they form a unique fingerprint.

Cite this