Date of Award

1-1-2018

Language

English

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

College/School/Department

Department of Computer Science

Content Description

1 online resource (ix, 55 pages) : illustrations (some color)

Dissertation/Thesis Chair

PALIATH NARENDRAN

Committee Members

NEIL V MURRAY, RICHARD E STEARNS

Keywords

ASYMMETRIC UNIFICATION, DECIDABILITY AND UNDECIDABILITY, DISUNIFICATION, EQUATIONAL UNIFICATION, TIME COMPLEXITY ANALYSIS, Logic programming, Rewriting systems (Computer science), Equations, Computational complexity

Subject Categories

Computer Sciences

Abstract

We compare two kinds of unification problems: asymmetric unification and disunification, which are variants of equational unification. Asymmetric unification is a type of equational unification where the solutions keep the right-hand sides of the equations in normal form with respect to the given term rewriting system. In disunification we solve equations and disequations with respect to an equational theory. We contrast the time complexities and decidability of both and show that the two problems are incomparable: there are theories where one is decidable whereas the other is undecidable; for theories which are decidable we show one can be solved in polynomial time while the other is NP-hard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.

Share

COinS