Geodesic
Restricted ideals and the groupability property. Tools for temporal reasoning
Kybernetika, Tome 39 (2003) no. 5, pp. 521-546 Cet article a éte moissonné depuis la source Czech Digital Mathematics Library

Voir la notice de l'article

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.
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.
Classification : 03B35, 03B44, 03D70, 03G10, 06A15, 68T15
Keywords: lattice; ideal; induction; temporal reasoning; prime implicants/implicates 
@article{KYB_2003_39_5_a2,
     author = {Mart{\'\i}nez, J. and Cordero, P. and Guti\'errez, G. and Guzm\'an, I. P. de},
     title = {Restricted ideals and the groupability property. {Tools} for temporal reasoning},
     journal = {Kybernetika},
     pages = {521--546},
     year = {2003},
     volume = {39},
     number = {5},
     mrnumber = {2042339},
     zbl = {1249.03004},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/KYB_2003_39_5_a2/}
}
TY  - JOUR
AU  - Martínez, J.
AU  - Cordero, P.
AU  - Gutiérrez, G.
AU  - Guzmán, I. P. de
TI  - Restricted ideals and the groupability property. Tools for temporal reasoning
JO  - Kybernetika
PY  - 2003
SP  - 521
EP  - 546
VL  - 39
IS  - 5
UR  - http://geodesic.mathdoc.fr/item/KYB_2003_39_5_a2/
LA  - en
ID  - KYB_2003_39_5_a2
ER  - 
%0 Journal Article
%A Martínez, J.
%A Cordero, P.
%A Gutiérrez, G.
%A Guzmán, I. P. de
%T Restricted ideals and the groupability property. Tools for temporal reasoning
%J Kybernetika
%D 2003
%P 521-546
%V 39
%N 5
%U http://geodesic.mathdoc.fr/item/KYB_2003_39_5_a2/
%G en
%F KYB_2003_39_5_a2
Martínez, J.; Cordero, P.; Gutiérrez, G.; Guzmán, I. P. de. Restricted ideals and the groupability property. Tools for temporal reasoning. Kybernetika, Tome 39 (2003) no. 5, pp. 521-546. http://geodesic.mathdoc.fr/item/KYB_2003_39_5_a2/

[1] Abiteboul S., Vianu V.: Non-determinism in logic based languages. Ann. Math. Artif. Intell. 3 (1991), 151–186 | DOI | MR | Zbl

[2] Corciulo L., Giannotti F., Pedreschi, D., Zaniolo C.: Expressive power of non-deterministic operators for logic-based languages. Workshop on Deductive Databases and Logic Programming, 1994, pp. 27–40

[3] Cordero P., Enciso, M., Guzmán I. de: Structure theorems for closed sets of implicates/implicants in temporal logic. (Lecture Notes in Artificial Intelligence 1695.) Springer–Verlag, Berlin 1999 | Zbl

[4] Cordero P., Enciso, M., Guzmán I. de: A temporal negative normal form which preserves implicants and implicates. J. Appl. Non-Classical Logics 10 (2000), 3–4, 243–272 | DOI | MR | Zbl

[5] Cordero P., Enciso, M., Guzmán I. de: From the posets of temporal implicates/implicants to a temporal negative normal form. Rep. Math. Logic 36 (2002), 3–48

[6] Cordero P., Enciso, M., Guzmán I. de: Bases for closed sets of implicants and implicates in temporal logic. Acta Inform. 38 (2002), 599–619 | DOI | MR | Zbl

[7] Cordero P., Enciso M., Guzmán, I. de, Martínez J.: A New algebraic tool for automatic theorem provers. Ann. Math. Artif. Intell. (to appear)

[8] Guzmán I. de, Ojeda, M., Valverde A.: Reductions for non-clausal theorem proving. Theoret. Comput. Sci. 266 (2001), 1–2, 81–112 | DOI | MR | Zbl

[9] Dix A. J.: Non-determinism as a paradigm for understanding the user interface. Chapter 4 in Formal Methods in Human-Computer Iteraction. Cambridge University Press, Cambridge 1990, pp. 97–127

[10] Giannoti F., Pedreschi D., Sacca, D., Zaniolo C.: Non-determinism in deductive databases. Proc. 2nd Internat. Conference on Deductive and Object-Oriented Databases, 1991

[11] Grätzer G.: General Lattice Theory. Second edition. Birkhäuser, Basel 1998 | MR

[12] Gutiérrez G., Guzmán I. de, Martínez J., Ojeda, M., Valverde A.: Reduction Theorems for Boolean Formulas Using $\Delta $-Trees. Springer Verlag, Berlin 2000 | MR | Zbl

[13] Gutiérrez G., Guzmán I. de, Martínez J., Ojeda, M., Valverde A.: Satisfiability testing for Boolean formulas using $\Delta $-trees. Studia Folder | Zbl

[14] Hänle R., Escalada G.: Deduction in many valued logics: a survey. Mathware and Soft Computing, 1997 | MR

[15] Hänle R.: Advances in Many-Valued Logics. Kluwer, Dordrecht 1999

[16] Jackson P., Pais J.: Computing Prime Implicants. (Lecture Notes in Artificial Intelligence 449.) Spriger-Verlag, Berlin 1990, pp. 543–557 | MR

[17] Kean A.: The approximation of implicates and explanations. Internat. J. Approx. Reason. 9 (1993), 97–128 | DOI | MR | Zbl

[18] Kean A., Tsiknis G.: An incremental method for generating prime implicants/implicates. J. Symbolic Comput. 9 (1990), 185–206 | DOI | MR | Zbl

[19] Kleer J. de, Mackworth A. K., Reiter R.: Characterizing diagnoses and systems. Artif. Intell. 56 (1992), 2–3, 192–222 | DOI | MR | Zbl

[20] Kogan A., Ibaraki, T., Makino K.: Functional dependencies in horn theories. Artif. Intell. 108 (1999), 1–30 | DOI | MR | Zbl

[21] Marquis P.: Extending abduction from propositional to first-order logic. Fund. Artif. Intell. Res. 1991, pp. 141–155 | DOI | MR | Zbl

[22] Martínez J.: $\Omega $-álgebras con onds. Doctoral Dissertation, University of Málaga, 2000

[23] Martínez J., Gutierrez G., Guzmán I. P. de, Cordero P.: Multilattices looking at computations. Discrete Mathematics (to appear)

[24] Mishchenko A., Brayton R.: Theory of non-deterministic networks. An International Workshop on Boolean Problems, 2002

[25] Tomite M.: Efficient Parsing for Natural Language. Kluwer, Dordrecht 1986