Article
Full entry |
PDF
(2.7 MB)
Feedback
PDF
(2.7 MB)
Feedback
Keywords:
lattice; ideal; induction; temporal reasoning; prime implicants/implicates
lattice; ideal; induction; temporal reasoning; prime implicants/implicates
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.
References:
[1] Abiteboul S., Vianu V.: Non-determinism in logic based languages. Ann. Math. Artif. Intell. 3 (1991), 151–186 DOI 10.1007/BF01530924 | MR 1219407 | Zbl 0875.68586
[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 0961.03020
[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 10.1080/11663081.2000.10510999 | MR 1915686 | Zbl 1033.03507
[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 10.1007/s00236-002-0087-2 | MR 1918510 | Zbl 1034.68087
[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 10.1016/S0304-3975(00)00044-X | MR 1850266 | Zbl 0989.68128
[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 1670580
[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 1872894 | Zbl 0998.03006
[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
[14] Hänle R., Escalada G.: Deduction in many valued logics: a survey. Mathware and Soft Computing, 1997 MR 1621902
[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 1077022
[17] Kean A.: The approximation of implicates and explanations. Internat. J. Approx. Reason. 9 (1993), 97–128 DOI 10.1016/0888-613X(93)90015-6 | MR 1237301 | Zbl 0784.68085
[18] Kean A., Tsiknis G.: An incremental method for generating prime implicants/implicates. J. Symbolic Comput. 9 (1990), 185–206 DOI 10.1016/S0747-7171(08)80029-6 | MR 1056843 | Zbl 0704.68100
[19] Kleer J. de, Mackworth A. K., Reiter R.: Characterizing diagnoses and systems. Artif. Intell. 56 (1992), 2–3, 192–222 DOI 10.1016/0004-3702(92)90027-U | MR 1187356 | Zbl 0772.68085
[20] Kogan A., Ibaraki, T., Makino K.: Functional dependencies in horn theories. Artif. Intell. 108 (1999), 1–30 DOI 10.1016/S0004-3702(98)00114-3 | MR 1681039 | Zbl 0914.68185
[21] Marquis P.: Extending abduction from propositional to first-order logic. Fund. Artif. Intell. Res. 1991, pp. 141–155 DOI 10.1007/3-540-54507-7_12 | MR 1227997 | Zbl 0793.03007
[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
Search
Partner of
