Abstract
A new type of tableau system is proposed for the complete class (called miniscoped Horn-like) of first-order linear temporal logic. The described system instead of induction-like postulates contains some nonlogical axioms indicating the saturation of a derivation process in this system.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Fisher, M.:A Resolution Method for Temporal Logic, Proc. IJCAI, Sydney, 1991
Fitting, M.:First-Order Logic and Automated Theorem Proving, Springer-Verlag, Berlin, 1990.
Gallier, J. H.:Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York, 1986.
Kawai, H.: Sequential calculus for a first order infinitary temporal logic,Zeitshr. für Math. Logic und Grundlagen der Math. 33 (1987), 423–432.
Pliuškevičius, R.: Investigation of finitary calculi for temporal logic by means of infinitary calculi, in B. Rovan (ed.),Mathematical Foundations of Computer Science 1990, Lecture Notes in Comput. Sci., 452, Springer-Verlag, Berlin, 1990, pp. 464–469.
Pliuškevičius, R.: On saturated calculi for a linear temporal logic, in A. Borzyszkowski and S. Sokolowski (eds),Mathematical Foundations of Computer Science 1993, Lecture Notes in Comput. Sci., 711, Springer-Verlag, 1993, pp. 640–649.
Pliuškevičius, R.: On the saturation principle for a linear temporal logic, in G. Gottlob, A. Leitsch and D. Mundici (eds),Computational Logic and Proof Theory, Lecture Notes in Comput. Sci., 713, Springer-Verlag, Berlin, 1993, pp. 289–300.
Pratt, V. R.: A practical decision method for propositional dynamic logic,ACM Symp. on Theory of Computing, 1978, 326–337.
Sundholm, G.: Systems of deduction, in D. Gabbay and F. Guenthner (eds),Handbook of Philosophical Logics, vol. 1, D. Reidel, Dordrecht, 1983, pp. 138–188.
Valiev, M.: On temporal logic of von Wright (in Russian),The second Soviet-Finland Colloquium on Logic, Moscow, 1979, pp. 7–11.
Wolper, P.: The tableaux method for temporal logic: an overview,Log. et anal. 28 (1985), 119–136.
Zeman, J. J.:Modal Logic: The Lewis-Modal Systems, Oxford University Press, Oxford, 1973.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Pliuškevičius, R. The saturated tableaux for linear miniscoped horn-like temporal logic. J Autom Reasoning 13, 391–407 (1994). https://doi.org/10.1007/BF00881951
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00881951