On the complexity of Boolean unification

Unification modulo the theory of Boolean algebras has been investigated by several autors. Nevertheless, the exact complexity of the decision problem for unification with constants and general unification was not known. In this research note, we show that the decision problem is Π 2 p -complete for...

Full description

Saved in:
Bibliographic Details
Published in:Information processing letters 1998-08, Vol.67 (4), p.215-220
Main Author: Baader, Franz
Format: Article
Language:English
Subjects:
Algebra
Algorithmics. Computability. Computer arithmetics
Applied sciences
Artificial intelligence
Automatic theorem proving
Boolean
Computational complexity
Computer science
control theory
systems
Exact sciences and technology
Information processing
Logical, boolean and switching functions
Problem solving, game playing
Studies
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Unification modulo the theory of Boolean algebras has been investigated by several autors. Nevertheless, the exact complexity of the decision problem for unification with constants and general unification was not known. In this research note, we show that the decision problem is Π 2 p -complete for unification with constants and PSPACE-complete for general unification. In contrast, the decision problem for elementary unification (where the terms to be unified contain only symbols of the signature of Boolean algebras) is “only” NP-complete.
ISSN:0020-0190
1872-6119
DOI:10.1016/S0020-0190(98)00106-9