Restricted ideals and the groupability property. Tools for temporal reasoning

uncategorised
Authors

Javier Martínez

Pablo Cordero

Gloria Gutiérrez

Inma P. de Guzmán

Published

1 January 2003

Publication details

Kybernetika vol. 39 (5), pages 521–546.

Links

 

Abstract

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 [17, 19, 20, 21]. 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 [3, 4, 5, 6]. 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.

Citation

Please, cite this work as:

[Mar+03] J. Mart', P. Cordero, G. Gutiérrez, et al. “Restricted ideals and the groupability property. Tools for temporal reasoning”. In: Kybernetika 39.5 (2003), pp. 521-546. URL: http://www.kybernetika.cz/content/2003/5/521.

@Article{Martinez2003,
     author = {Javier Mart'and Pablo Cordero and Gloria Guti{’e}rrez and Inman P. {de Guzm{’a}n}},
     journal = {Kybernetika},
     title = {Restricted ideals and the groupability property. Tools for temporal reasoning},
     year = {2003},
     number = {5},
     pages = {521–546},
     volume = {39},
     abstract = {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 [17, 19, 20, 21]. 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 [3, 4, 5, 6]. 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.},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/kybernetika/MartinezCGG03.bib},
     timestamp = {Tue, 29 Aug 2023 01:00:00 +0200},
     url = {http://www.kybernetika.cz/content/2003/5/521},
}