Undecidability of satisfiability in the algebra of finite binary relations with union, composition, and difference

TL;DR

This paper proves that determining finite satisfiability of expressions built from binary relations with union, composition, and difference is undecidable, even with limited operators and a single relation.

Contribution

It establishes the undecidability of finite satisfiability for a restricted algebra of binary relations, extending the understanding of logical expressiveness and computational limits.

Findings

Finite satisfiability is undecidable for the algebra with union, composition, and difference.

Undecidability holds even with a single relation name and limited nesting of difference.

The result impacts the understanding of the computational complexity of reasoning in relation algebras.

Abstract

We consider expressions built up from binary relation names using the operators union, composition, and set difference. We show that it is undecidable to test whether a given such expression $e$ is finitely satisfiable, i.e., whether there exist finite binary relations that can be substituted for the relation names so that $e$ evaluates to a nonempty result. This result already holds in restriction to expressions that mention just a single relation name, and where the difference operator can be nested at most once.