From the poset of literals to a temporal negative normal form

• Autorzy: Cordero P. , Enciso M. , Guzman I.
• Języki publikacji: EN

Abstrakty

EN

Linear time temporal logics have proven to yield successful formalisms for a wide range of applications. Nevertheless, the lack of an efficient automated deduction method has prevented temporal logics from playing a more important role in computer science. Recently, the use of unitary implicates and implicants has guided a lot of work in automated deduction. In this paper, we present a formal framework in the study of unitary implicants and implicates in Temporal Logic. It is focussed on the temporal propositional logic, FNext+ -, with an infinite, linear and discrete flow of time. In our opinion, this formal framework allows an outstanding advance in the search for efficient automated deduction methods in temporal logics. The sets of unitary implicates and implicants of a formula in FNext+ - can be infinite and therefore difficult to handle. We introduce the notion of temporal literal in FNext+ - and we consider the semantic implication as an order relation over the set of temporal literals. Then, we develop theoretical studies of the poset of temporal literals and the sets of implicants and implicates. The formal results obtained allow us to define an efficient way to extract the maximum amount of information about the set of unitary implicants and implicates of the formula. To emphasize the interest of these theoretical results, we show how this study allows us to introduce a suitable notion of Temporal Negative Normal Form for Temporal Logic. The definition of such a normal form constitutes an unsolved problem until now. This is a major contribution of the paper and it will have a significant relevance in the future design of efficient automated theorem provers.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2002
• Tom: No. 36
• Strony: 3--53
• Opis fizyczny: Bibliogr. 23 poz., rys.

Twórcy

autor

Cordero P.

• E.T.S.I. Informatica Universidad de Malaga Campus de Teatinos s/n 29071 Malaga Spain

autor

Enciso M.

• E.T.S.I. Informatica Universidad de Malaga Campus de Teatinos s/n 29071 Malaga Spain

autor

Guzman I.

• E.T.S.I. Informatica Universidad de Malaga Campus de Teatinos s/n 29071 Malaga Spain

Bibliografia

• [1] M. D’Agostino, D. M. Gabbay, R. Hahnle, J. Possega, Handbook of Tableau Methods, Kluwer Academic Publishers, 1999.
• [2] C. Dixon, Search Strategies for Resolution in Temporal Logics, in: 12th International Joint Conference on Artificial Intelligence (IJCAI), 1991.
• [3] M. Fisher, A resolution method for temporal logic, in: 12th International Joint Conference on Artificial Intelligence (IJCAI), 1991.
• [4] M. Fisher, A normal form for temporal logic and its applications in theorem proving, Journal of Logic and Computation, 7(4) (1997), 429–456.
• [5] I. P. de Guzmán, G. Aguilera and M. Ojeda, Increasing the efficiency of automated theorem proving, Journal of Applied Non-Classical Logics, 5(1) (1995), 9–29.
• [6] I. P. de Guzmán, G. Aguilera and M. Ojeda, A reduction-based theorem prover for 3-valued logic, Mathware & Soft Computing, IV(2) (1997), 99–127.
• [7] I. P. de Guzmán, G. Aguilera, M. Ojeda and A. Valverde, Reducing signed propositional formulas, Soft Computing, 2(4) (1998).
• [8] I. P. de Guzmán and M. Enciso, A new and complete automated theorem prover for temporal logic, IJCAI-Workshop on Executable Temporal Logics, 1995.
• [9] I. P. de Guzmán, M. Enciso and C. Rossi, Temporal reasoning over linear discrete time, Lect. Notes in Artif. Intelligence no. 1124 (1996), 198–216.
• [10] I. P. de Guzmán, P. Cordero and M. Enciso, Structure Theorems for Implicants and Implicates, in: Progress in Artificial intelligence, Lect. Notes in Artif. Intelligence Vol 1695 (1999).
• [11] H. Kamp, Tense logic and theory of linear orders, PhD Thesis. University of California, Los Angeles, 1968.
• [12] J. de Kleer, A. K. Mackworth, and R. Reiter, Characterizing diagnoses and systems, Artificial Intelligence, 56 (2–3) (1992), 192–222.
• [13] Z. Manna and A. Pnueli, Temporal verification of reactive systems: Safety. SpringerVerlag, 1995.
• [14] N.V. Murray, E. Rossenthal, Dissolution: Making Paths Vanish, Journal of the ACM, Vol. 40, Num. 3. July 1993, 504–535.
• [15] D. A. Plaisted and S. Greenbaum, A structure-preserving clause form translation, Journal of Symbolic Computation, 2 (1986), 293–304.
• [16] A. G. Ramesh, Some applications of non-clausal deduction, PhD thesis, Department of Computer Science, State University of New York at Albany, 1995.
• [17] A. G. Ramesh, G. Becker, and N. V. Murray, Cnf and dnf considered harmful for computing prime implicants/implicates, Journal of Automated Reasoning, to appear.
• [18] A. G. Ramesh, B. Beckert, R. Hanle, and N. V. Murray, Fast subsumption checks using anti-links, Journal of Automated Reasoning, 1996.
• [19] D. Scott, The Logic of Tenses, Standford, 1965.
• [20] T. Ssaso, Logic synthesis and optimization, Kluver, Norwell (USA), 1993.
• [21] P. Wolper, The tableaux method for temporal logic: an overview, Logique et Analyse, 28 année (1985), 110-111:119–136.
• [22] G.H. von Wright, And Next, Acta Philosophica Fennica, 1965.
• [23] G.H. von Wright, Philosophical Logic (Philosophical Papers), Vol II, Oxford, Blackwell, 1983.