Restricted ideals and the groupability property. Tools for temporal reasoning

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

Kybernetika (2003)

  • Volume: 39, Issue: 5, page [521]-546
  • ISSN: 0023-5954

Abstract

top
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.

How to cite

top

Martínez, J., et al. "Restricted ideals and the groupability property. Tools for temporal reasoning." Kybernetika 39.5 (2003): [521]-546. <http://eudml.org/doc/33663>.

@article{Martínez2003,
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. 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.},
author = {Martínez, J., Cordero, P., Gutiérrez, G., Guzmán, I. P. de},
journal = {Kybernetika},
keywords = {lattice; ideal; induction; temporal reasoning; prime implicants/implicates; lattice; ideal; induction; temporal reasoning; prime implicants; prime implicates},
language = {eng},
number = {5},
pages = {[521]-546},
publisher = {Institute of Information Theory and Automation AS CR},
title = {Restricted ideals and the groupability property. Tools for temporal reasoning},
url = {http://eudml.org/doc/33663},
volume = {39},
year = {2003},
}

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
PB - Institute of Information Theory and Automation AS CR
VL - 39
IS - 5
SP - [521]
EP - 546
AB - 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.
LA - eng
KW - lattice; ideal; induction; temporal reasoning; prime implicants/implicates; lattice; ideal; induction; temporal reasoning; prime implicants; prime implicates
UR - http://eudml.org/doc/33663
ER -

References

top
  1. Abiteboul S., Vianu V., 10.1007/BF01530924, Ann. Math. Artif. Intell. 3 (1991), 151–186 (1991) Zbl0875.68586MR1219407DOI10.1007/BF01530924
  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 (1994) 
  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 Zbl0961.03020
  4. Cordero P., Enciso, M., Guzmán I. de, 10.1080/11663081.2000.10510999, J. Appl. Non-Classical Logics 10 (2000), 3–4, 243–272 Zbl1033.03507MR1915686DOI10.1080/11663081.2000.10510999
  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, 10.1007/s00236-002-0087-2, Acta Inform. 38 (2002), 599–619 Zbl1034.68087MR1918510DOI10.1007/s00236-002-0087-2
  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., 10.1016/S0304-3975(00)00044-X, Theoret. Comput. Sci. 266 (2001), 1–2, 81–112 Zbl0989.68128MR1850266DOI10.1016/S0304-3975(00)00044-X
  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 (1990) 
  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 MR1670580
  12. Gutiérrez G., Guzmán I. de, Martínez J., Ojeda, M., Valverde A., Reduction Theorems for Boolean Formulas Using Δ -Trees, Springer Verlag, Berlin 2000 Zbl0998.03006MR1872894
  13. Gutiérrez G., Guzmán I. de, Martínez J., Ojeda, M., Valverde A., Satisfiability testing for Boolean formulas using Δ -trees, Studia Folder Zbl1017.03003
  14. Hänle R., Escalada G., Deduction in many valued logics: a survey, Mathware and Soft Computing, 1997 MR1621902
  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 (1990) MR1077022
  17. Kean A., 10.1016/0888-613X(93)90015-6, Internat. J. Approx. Reason. 9 (1993), 97–128 (1993) Zbl0784.68085MR1237301DOI10.1016/0888-613X(93)90015-6
  18. Kean A., Tsiknis G., 10.1016/S0747-7171(08)80029-6, J. Symbolic Comput. 9 (1990), 185–206 (1990) Zbl0704.68100MR1056843DOI10.1016/S0747-7171(08)80029-6
  19. Kleer J. de, Mackworth A. K., Reiter R., 10.1016/0004-3702(92)90027-U, Artif. Intell. 56 (1992), 2–3, 192–222 (1992) Zbl0772.68085MR1187356DOI10.1016/0004-3702(92)90027-U
  20. Kogan A., Ibaraki, T., Makino K., 10.1016/S0004-3702(98)00114-3, Artif. Intell. 108 (1999), 1–30 (1999) Zbl0914.68185MR1681039DOI10.1016/S0004-3702(98)00114-3
  21. Marquis P., 10.1007/3-540-54507-7_12, Fund. Artif. Intell. Res. 1991, pp. 141–155 (1991) Zbl0793.03007MR1227997DOI10.1007/3-540-54507-7_12
  22. Martínez J., Ω -á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 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.