Ordered direct implicational basis of a finite closure system

TL;DR

This paper introduces the ordered direct basis, or D-basis, for finite closure systems, enabling efficient closure computation and optimization in logic programming by prescribing an order to implications.

Contribution

It presents the concept of the ordered direct basis, details its extraction from direct unit bases, and demonstrates its advantages for optimizing forward chaining in logic programming.

Findings

D-basis can be extracted in polynomial time

Ordered D-basis optimizes forward chaining

Not all canonical bases are ordered direct

Abstract

Closure system on a finite set is a unifying concept in logic programming, relational data bases and knowledge systems. It can also be presented in the terms of finite lattices, and the tools of economic description of a finite lattice have long existed in lattice theory. We present this approach by describing the so-called D-basis and introducing the concept of ordered direct basis of an implicational system. A direct basis of a closure operator, or an implicational system, is a set of implications that allows one to compute the closure of an arbitrary set by a single iteration. This property is preserved by the D-basis at the cost of following a prescribed order in which implications will be attended. In particular, using an ordered direct basis allows to optimize the forward chaining procedure in logic programming that uses the Horn fragment of propositional logic. One can extract the D-basis from any direct unit basis S in time polynomial in the size of S, and it takes only linear time of the cardinality of the D-basis to put it into a proper order. We produce examples of closure systems on a 6-element set, for which the canonical basis of Duquenne and Guigues is not ordered direct.