Kybernetika 39 no. 5, 521-546, 2003

Restricted ideals and the groupability property. Tools for temporal reasoning

J. Martínez, P. Cordero, G. Gutiérrez and I. P. de Guzmán


In the field of automatic proving, the study of the sets of prime implicants or implicates of a formula has proven to be very important. If we focus on non-classical logics and, in particular, on temporal logics, such study is useful even if it is restricted to the set of unitary implicants/implicates [P. Cordero, M. Enciso, and I. de Guzmán: Structure theorems for closed sets of implicates/implicants in temporal logic. (Lecture Notes in Artificial Intelligence 1695.) Springer-Verlag, Berlin 1999]. In this paper, a new concept we call { restricted ideal/filter} is introduced, it is proved that the set of restricted ideals/filters with the relation of inclusion has lattice structure and its utility for the efficient manipulation of the set of unitary implicants/implicates of formulas in propositional temporal logics is shown. We introduce a new property for subsets of lattices, which we call { groupability}, and we prove that the existence of { groupable} subsets in a lattice allows us to express restricted ideals/filters as the inductive closure for a binary non-deterministic operator and, consequently, the presence of this property guarantees a proper computational behavior of the set of unitary implicants/implicates.