| Title:
|
Restricted ideals and the groupability property. Tools for temporal reasoning (English) |
| Author:
|
Martínez, J. |
| Author:
|
Cordero, P. |
| Author:
|
Gutiérrez, G. |
| Author:
|
Guzmán, I. P. de |
| Language:
|
English |
| Journal:
|
Kybernetika |
| ISSN:
|
0023-5954 |
| Volume:
|
39 |
| Issue:
|
5 |
| Year:
|
2003 |
| Pages:
|
[521]-546 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
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. (English) |
| Keyword:
|
lattice |
| Keyword:
|
ideal |
| Keyword:
|
induction |
| Keyword:
|
temporal reasoning |
| Keyword:
|
prime implicants/implicates |
| MSC:
|
03B35 |
| MSC:
|
03B44 |
| MSC:
|
03D70 |
| MSC:
|
03G10 |
| MSC:
|
06A15 |
| MSC:
|
68T15 |
| idZBL:
|
Zbl 1249.03004 |
| idMR:
|
MR2042339 |
| . |
| Date available:
|
2009-09-24T19:56:29Z |
| Last updated:
|
2015-03-24 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/135553 |
| . |
| Reference:
|
[1] Abiteboul S., Vianu V.: Non-determinism in logic based languages.Ann. Math. Artif. Intell. 3 (1991), 151–186 Zbl 0875.68586, MR 1219407, 10.1007/BF01530924 |
| Reference:
|
[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 |
| Reference:
|
[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 0961.03020 |
| Reference:
|
[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 Zbl 1033.03507, MR 1915686, 10.1080/11663081.2000.10510999 |
| Reference:
|
[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 |
| Reference:
|
[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 Zbl 1034.68087, MR 1918510, 10.1007/s00236-002-0087-2 |
| Reference:
|
[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) |
| Reference:
|
[8] Guzmán I. de, Ojeda, M., Valverde A.: Reductions for non-clausal theorem proving.Theoret. Comput. Sci. 266 (2001), 1–2, 81–112 Zbl 0989.68128, MR 1850266, 10.1016/S0304-3975(00)00044-X |
| Reference:
|
[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 |
| Reference:
|
[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 |
| Reference:
|
[11] Grätzer G.: General Lattice Theory.Second edition. Birkhäuser, Basel 1998 MR 1670580 |
| Reference:
|
[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 Zbl 0998.03006, MR 1872894 |
| Reference:
|
[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 1017.03003 |
| Reference:
|
[14] Hänle R., Escalada G.: Deduction in many valued logics: a survey.Mathware and Soft Computing, 1997 MR 1621902 |
| Reference:
|
[15] Hänle R.: Advances in Many-Valued Logics.Kluwer, Dordrecht 1999 |
| Reference:
|
[16] Jackson P., Pais J.: Computing Prime Implicants.(Lecture Notes in Artificial Intelligence 449.) Spriger-Verlag, Berlin 1990, pp. 543–557 MR 1077022 |
| Reference:
|
[17] Kean A.: The approximation of implicates and explanations.Internat. J. Approx. Reason. 9 (1993), 97–128 Zbl 0784.68085, MR 1237301, 10.1016/0888-613X(93)90015-6 |
| Reference:
|
[18] Kean A., Tsiknis G.: An incremental method for generating prime implicants/implicates.J. Symbolic Comput. 9 (1990), 185–206 Zbl 0704.68100, MR 1056843, 10.1016/S0747-7171(08)80029-6 |
| Reference:
|
[19] Kleer J. de, Mackworth A. K., Reiter R.: Characterizing diagnoses and systems.Artif. Intell. 56 (1992), 2–3, 192–222 Zbl 0772.68085, MR 1187356, 10.1016/0004-3702(92)90027-U |
| Reference:
|
[20] Kogan A., Ibaraki, T., Makino K.: Functional dependencies in horn theories.Artif. Intell. 108 (1999), 1–30 Zbl 0914.68185, MR 1681039, 10.1016/S0004-3702(98)00114-3 |
| Reference:
|
[21] Marquis P.: Extending abduction from propositional to first-order logic.Fund. Artif. Intell. Res. 1991, pp. 141–155 Zbl 0793.03007, MR 1227997, 10.1007/3-540-54507-7_12 |
| Reference:
|
[22] Martínez J.: $\Omega $-álgebras con onds.Doctoral Dissertation, University of Málaga, 2000 |
| Reference:
|
[23] Martínez J., Gutierrez G., Guzmán I. P. de, Cordero P.: Multilattices looking at computations.Discrete Mathematics (to appear) |
| Reference:
|
[24] Mishchenko A., Brayton R.: Theory of non-deterministic networks.An International Workshop on Boolean Problems, 2002 |
| Reference:
|
[25] Tomite M.: Efficient Parsing for Natural Language.Kluwer, Dordrecht 1986 |
| . |
