Treffer: Set-Term Unification in a Logic Database Language

Deterministic, parallel set-term unification algorithms for high-order logic-based database languages, of which set terms have the commutative and idempotent properties, are lacking. As a result, an efficient inference mechanism that can be used to determine answers to queries of these database languages deterministically is nonexistent. To overcome these shortcomings, we propose a set-term unification algorithm for LDL=NR, a high-order logic database language. The proposed algorithm not only computes all generalized ground unifiers (ggu s ) of a given pair of set terms in LDL=NR without duplicates but also takes the advantage of existing multiple processors for computing all these unifiers in parallel. The proofs of correctness and computational complexity of the proposed algorithm are also included in this paper. Keywords: Logic database language, combinatorics, set term, logic programming, unification. 1 Introduction High-order logic-based database languages, such as HILOG [CC90].