×

zbMATH — the first resource for mathematics

Representing any-time and program-iteration by infinitary conjunction. (English) Zbl 1398.03094
Summary: Two new infinitary modal logics are simply obtained from a Gentzen-type sequent calculus for infinitary logic by adding a next-time operator, and a program operator, respectively. It is shown that an any-time operator and a program-iteration operator can respectively be expressed using infinitary conjunction in these logics. The cut-elimination and completeness theorems for these logics are proved using some theorems for embedding these logics into (classical) infinitary logic.
MSC:
03B45 Modal logic (including the logic of norms)
03C75 Other infinitary logic
03F05 Cut-elimination and normal-form theorems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barwise, J., & Feferman, S. (Eds.) (1985). Model-theoretic logics (Perspectives in Mathematical Logics, Vol. 8). Berlin: Springer. · Zbl 0587.03001
[2] Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., & Zhu, Y. (2003). Bounded model checking. Advances in Computers,58, 118-149.
[3] Cerrito, S., Mayer, M. C., & Prand, S. (1999). First order linear temporal logic over finite time structures. In H. Ganzinger, D. A. McAllester & A. Voronkov (Eds.), Logic Programming and Automated Reasoning, 6th International Conference, LPAR’99, Tbilisi, Georgia, September 6-10, 1999, Proceedings (pp. 62-76). Berlin: Springer. · Zbl 0939.03022
[4] Emerson, E. A. (1990). Temporal and modal logic. In J. van Leeuwen (Ed.), Handbook of theoretical computer science, vol. B: Formal models and semantics (pp. 995-1072). Cambridge, MA: MIT Press. · Zbl 0900.03030
[5] Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995). Reasoning about knowledge. Cambridge, MA: MIT Press. · Zbl 0839.68095
[6] Harel, D., Kozen, D., & Tiuryn, J. (2000). Dynamic logic (Foundations of Computing). Cambridge, MA: MIT Press. · Zbl 0976.68108
[7] Kamide, N. (2009). Embedding linear-time temporal logic into infinitary logic: Application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic. In M. Fisher, F. Sadri, & M. Thielscher (Eds.), Computational Logic in Multi-Agent Systems, 9th International Workshop, CLIMA IX, Dresden, Germany, September 29-30, 2008. Revised selected and invited papers (pp. 57-76). Berlin: Springer. · Zbl 1250.03028
[8] Kamide, N., & Wansing, H. (2010). Combining linear-time temporal logic with constructiveness and paraconsistency. Journal of Applied Logic,8, 33-61. · Zbl 1207.03022
[9] Prior, A. N. (1957). Time and modality. Oxford: Clarendon Press. · Zbl 0079.00606
[10] Prior, A. N. (1967). Past, present and future. Oxford: Clarendon Press. · Zbl 0169.29802
[11] Takeuti, G. (1975). Proof theory. Amsterdam: North-Holland. · Zbl 0354.02027
[12] Benthem, J. (1999). Modality, bisimulation and interpolation in infinitary logic. Annals of Pure and Applied Logic,96, 29-41. · Zbl 0923.03048
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.