Distributive lattices with operators: resolution-based decision procedures and applications to knowledge representation
by
Viorica Sofronie-Stokkermans
Max-Planck-Institut für Informatik, Saarbrücken, Germany

It is known that representation and duality theorems for classes of algebraic structures allow, in many situations, to replace the algebraic structures by structured spaces which are in some sense simpler, or more tractable than the original algebras.

The goal of the present talk is twofold. On the one hand, we present several situations in which representation theorems for distributive lattices with operators can be used for obtaining efficient decision procedures for fragments of the first order theory of such classes of algebras (such as their universal theory and their positive theory). On the other hand, we point out some application domains in which decision procedures obtained this way proved useful, such as automated theorem proving in non classical logics and reasoning in terminological databases.

We first explain how extensions of the Priestley representation theorem allow to establish a natural link between the satisfiability of universal sentences with respect to classes of distributive lattices with operators (possibly many-sorted) and their satisfiability with respect to certain classes of relational structures. This justifies a method for translating universal sentences in such classes of algebras to a clause form which is usually much simpler. Refinements of resolution can then be used to obtain decision procedures. In particular, we obtained an exponential space and time decision procedure for the universal clause theory of the class of all bounded distributive lattices with operators (possibly satisfying a set of generalized residuation conditions), and a doubly-exponential time decision procedure for the universal clause theory of the class of all Heyting algebras.

The arguments above cannot be extended without modifications to other fragments of the first-order theory of such classes of algebras such as, for instance, their positive theory. However, we proved that the Priestley representation theorem allows to reduce testing satisfiability of unification problems with respect to the class of all bounded distributive lattices to the problem of checking the satisfiability of a set of clauses (this can be checked for instance by resolution). Similar results can be established for unification with linear constant restrictions. From this it follows that resolution can be used for deciding the positive theory of the class of all bounded distributive lattices. We will also discuss some possibilities of extending these ideas to more general classes of algebras.

Date received: February 27, 2003