Abstract
In this work we present a new Automated Theorem Prover, called TAS-FNext, applied to temporal logic. This is part of a broader project developed by our research group GIMAC. It is an extension of works [4], [5] and [6] concerns classical logic and [9] Minimal Temporal Logic.
TAS-FNext is strongly based on formula structures and, specifically, on the structure of the syntactic tree of each formula. It works by making transformations on these syntactic trees (TAS stands for Transformaciones de Árboles Sintácticos, Spanish rendering of Syntactic Tree Transformations).
The power of TAS-FNext is mainly based on its capacity to extract efficiently any potentially useful information contained in the syntactic trees with two aims: to detect and classify any subformulas found, whether or not they are valid, unsatisfiable, equivalent or equal, and to transform the formula in question into a simultaneous unsatisfiable, but with less size, formula.
TAS-FNext is sound and complete, and, moreover, it generates counter-models in a natural way [8].
The authors are members of GIMAC, a Computing research group of Málaga University. This work was partially supported by CICYT project TIC94-0847-C02-02.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Artosi and G. Governatori. Labeled model modal logic. In CADE12 Workshop on Automated Model Building. Springer-Verlag. LNAI, 1994. 838
M. Abadi and Z. Manna. Modal theorem proving. In Springer-Verlag, editor, 8th Int. Conf. on Automated Deduction. Lecture Notes in Computer Science, 1986.
M. Abadi and Z. Manna. Nonclausal deduction in first-order temporal logic. ACM Journal, 37(2):279–317, April 1990.
G. Aguilera, I.P. de Guzmán and M. Ojeda. Automated model building via syntactic trees transformations. In Proceedings of CADE-12 Workshop on Automated Model Building, pages 4–10, Nancy, France. June 1994.
G. Aguilera, I.P. de Guzmán and M. Ojeda. TAS-D++ syntactic trees transformations for automated theorem proving. Lectures Notes in Artifial Intelligence n. 838, pages 198–216. Sept 1994.
G. Aguilera, I.P. de Guzmán and M. Ojeda. Increasing the efficiency of automated theorem proving. Journal of Applied non-Classical logics 5 (1):9–29. 1995.
C. Dixon, M. Fisher, and R. Johnson. Parallel temporal resolution. In International Workshop on Temporal Representation and Reasoning TIME'95, Melbourne. Florida. EEUU, 1995.
M. Enciso. Demostración Automática de Teoremas: Eficiencia y Paralelismo. PhD thesis, Universidad de Málaga. España, 1995.
M. Enciso and I.P. de Guzmán. A new and complete Theorem Prover for Temporal Logic. In In Proceedings of IJCAI-95 Workshop on Executable Temporal Logics. Montreal, Canada. Aug. 1995.
M. Fitting. Destructive modal resolution. Journal of Logic and Computation, 1(1), 1990.
A. Galton, editor. Temporal Logic and Their Applications. Academic Press, 1987.
L. Fariñas del Cerro and A. Herzig. Modal Deduction with applications in Epistemic and Temporal Logics. Springer Verlag, 1991.
M. Fisher. A resolution method for temporal logic. In 12th International Joint Conference on Artificial Intelligence (IJCAI), Sydney. Australia, 1991.
G. Governatori. Labeled tableaux for multimodal logics. In 4th Workshop on Theorem Proving, Analytic Tableaux and Related Methods, Berlin. German, 1995. Springer-Verlag. LNAI. 918
R. Hahnle. Automated Deduction in Multiple-valued Logics. Oxford University Press, 1993.
R. Hahnle and O. Ibens. Improving temporal logic tableaux using integer constraints. In 1st International Conference on Temporal Logic. Springer-Verlag. LNAI., Munich. German, 1994. Vol. 827
R. Johnson. A blackboard approach to parallel temporal tableaux. In Artificial Intelligence Methodologies, Systems and Applications (AIMSA). World Scientific, 1994.
A. Massini. A Proof Theory of Modalities for Computer Science. PhD thesis, Universita di Pisa-Genova-Udine, Italy, 1993.
A. Ramsay. Formal Methods in Artificial Intelligence. Cambridge University Press, 1988.
F. Sanz. Hacia una alternativa a resolución. PhD thesis, Universidad de Málaga, Spain, 1992.
L. A. Wallen. Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. The MIT Press, Cambridge, Massachusetts, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Enciso, M., de Guzmán, I.P., Rossi, C. (1996). Temporal reasoning over linear discrete time. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds) Logics in Artificial Intelligence. JELIA 1996. Lecture Notes in Computer Science, vol 1126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61630-6_22
Download citation
DOI: https://doi.org/10.1007/3-540-61630-6_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61630-6
Online ISBN: 978-3-540-70643-4
eBook Packages: Springer Book Archive