Towards Massive Unification

Abstract

Unification is one of the fundamental operations in automated first-order reasoning and is used intensively in fields such as theorem proving or logic programming. Since Robinson’s pioneering proposal, several efficient algorithms using sophisticated data structures have been proposed, and some approaches to its parallelization have been analyzed. Recent advances in hardware give us the opportunity to work with large volumes of data. More specifically, the use of Graphical Processing Units (GPUs) is becoming increasingly common in applications not directly related to computer graphics. Among other requirements, the best performance of GPUs is achieved when working with data structures that exhibit large regularities, such as matrices. Unfortunately, this is not the case for inductively defined expressions, which are usually subject to unification in most applications. In this work, we present a proposal to efficiently solve large equality constraints using GPUs. For this purpose, we introduce a novel representation of equality constraints that does not suffer from irregularities.