×

zbMATH — the first resource for mathematics

A propositional probabilistic logic with discrete linear time for reasoning about evidence. (English) Zbl 1269.03033
The introduction and Section 2 of this paper are devoted to setting this paper in a wider context. To this end, the authors trace the combination of logic and probability back to Leibniz, Bernoulli, Laplace and other great historic figures. For the purposes of this paper the most relevant modern-day work is one of J. Y. Halpern and R. Pucella [J. Artif. Intell. Res. (JAIR) 26, 1–34 (2006; Zbl 1182.68244)] which contained an open question. This paper is aimed at answering this question.
In Section 3 the authors introduce a propositional logic which allows reasoning about evidence, prior and posterior probabilities, for which they define syntax and semantics. For a deducibility relation with countably many deduction steps the authors prove that the introduced logic is strongly complete.
The fourth section is devoted to a propositional logic for evidence and hypotheses that is enriched by two temporal operators, one operator for “next” and one operator for “until”. This logic is shown to be sound and strongly complete.
Section 5 contains the conclusions. Here the authors explain why their completeness results required infinitary inference rules by considering the example of polynomials of odd degree over the real numbers.

MSC:
03B62 Combined logics
03B44 Temporal logic
68T27 Logic in artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.: The power of temporal proofs. Theor. Comp. Sci. 65, 35–83 (1989) · Zbl 0669.03010 · doi:10.1016/0304-3975(89)90138-2
[2] Abadi, M.: Errata for ”The power of temporal proofs”. Theor. Comp. Sci. 70, 275 (1990) · Zbl 0701.03009 · doi:10.1016/0304-3975(90)90128-5
[3] Andréka, H., Németi, I., Sain, I.: On the strength of temporal proofs. Theor. Comp. Sci. 80, 125–151 (1991) · Zbl 0732.03020 · doi:10.1016/0304-3975(91)90386-G
[4] Burgess, J.: Axioms for tense logic I: since and until. Notre Dame J. Form. Log. 23(2), 367–374 (1982) · Zbl 0494.03013 · doi:10.1305/ndjfl/1093870149
[5] Burges, J.: Basic tense logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. II: Extensions of Classical Logic. Reidel Publishing Company, Dordrecht (1984)
[6] Doder, D., Ognjanović, Z., Marković, Z., Perović, A., Rašković, M: A probabilistic temporal logic that can model reasoning about evidence. In: FoIKS 2010, LNCS, vol. 5956, pp. 9–24 (2010)
[7] Doder, D., Ognjanović, Z., Marković, Z: An axiomatization of a first order branching time temporal logic. J. Univers. Comput. Sci. 16(11), 1439–1451 (2010) · Zbl 1216.03033
[8] Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 997–1072. Elsevier, Amsterdam (1990) · Zbl 0900.03030
[9] Emerson, E.: Automated temporal reasoning for reactive systems. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency, pp. 41–101. Springer (1996)
[10] Emerson, E., Halpern, J.: ’Sometimes’ and ’not never’ revisited: on branching versus linear time. J. ACM 33, 151–178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999
[11] Emerson, E., Sistla, A.: Deciding full branching time logic. Inf. Control 61, 175–201 (1984) · Zbl 0593.03007 · doi:10.1016/S0019-9958(84)80047-9
[12] Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. 7th ACM symp. Princ. of Prog. Lang., pp. 163–173 (1980)
[13] Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal logic. Mathematical Foundations and Computational Aspects, vol. 1. Clarendon Press (1994) · Zbl 0921.03023
[14] Fagin, R., Halpern, J., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput. 87(1–2), 78–128 (1990) · Zbl 0811.03014 · doi:10.1016/0890-5401(90)90060-U
[15] Halpern, J.: Reasoning about Uncertainty. The MIT Press (2003) · Zbl 1090.68105
[16] Leibnitz, G.W.: De conditionibus (1665)
[17] Leibnitz, G.W.: Specimen juris (1669)
[18] Leibnitz, G.W.: De Nouveaux essais (1765)
[19] Godo, L., Marchioni, E.: Coherent conditional probability in a fuzzy logic setting. Log. J. IGPL 14(3), 457–481 (2006) · Zbl 1117.03031 · doi:10.1093/jigpal/jzl019
[20] Hailperin, T.: Sentential Probability Logic, Origins, Development, Current Status, and Technical Applications. Lehigh University Press (1996) · Zbl 0922.03026
[21] Halpern, J., Fagin, R.: Two views of belief: belief as generalized probability and belief as evidence. Artif. Intell. 54, 275–317 (1992) · Zbl 0762.68055 · doi:10.1016/0004-3702(92)90048-3
[22] Halpern, J., Pucella, R.: A logic for reasoning about evidence. J. Artif. Intell. Res. 26, 1–34 (2006) · Zbl 1182.68244 · doi:10.1007/s10462-007-9045-2
[23] Hoover, D.N.: Probability logic. Ann. Math. Logic 14, 287–313 (1978) · Zbl 0394.03033 · doi:10.1016/0003-4843(78)90022-0
[24] Kaivola, R.: Axiomatising extended computation tree logic. In: Proceedings of 21st International Colloquium on Trees in Algebra and Programming, pp. 87–101 (1996) · Zbl 0893.68146
[25] Kamp, J.: Tense logic and the theory of linear order. Doctoral dissertation. University of California, Los Angeles (1968)
[26] Keisler, H.J.: Hyperfinite model theory. In: Gandy, R.O., Hyland, J.M.E. (eds.) Logic Colloquim 76, pp. 5–110. North-Holland (1977) · Zbl 0423.03041
[27] Keisler, H.J.: Probability quantifiers. In: Barwise, J., Feferman, S. (eds.) Model Theoretic Logics, pp. 509–556. Springer, Berlin (1985)
[28] Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Log. J. IGPL 8(1), 55–85 (2000) · Zbl 1033.03009 · doi:10.1093/jigpal/8.1.55
[29] Manna, Z., Pnueli, A.: Verification of concurrent programs: the temporal framework. In: Boyer, R.S., Moor, J.S. (eds.) The correctness problem in computer science, pp. 215–273. Academic, London (1981)
[30] Marković, Z., Ognjanović, Z., Rašković, M.: An intuitionistic logic with probabilistic operators. Publ. Inst. Math., Nouv. S’ er. 73(87), 31–38 (2003) · Zbl 1048.03020 · doi:10.2298/PIM0373031M
[31] Nilsson, N.: Probabilistic logic. Artif. Intell. 28, 71–87 (1986) · Zbl 0589.03007 · doi:10.1016/0004-3702(86)90031-7
[32] Nilsson, N.: Probabilistic logic revisited. Artif. Intell. 59, 39–42 (1993) · doi:10.1016/0004-3702(93)90167-A
[33] Ognjanović, Z., Rašković, M.: A logic with higher order probabilities. Publ. Inst. Math., Nouv. S’ er. 60(74), 1–4 (1996) · Zbl 1009.03513
[34] Ognjanović, Z.: Completeness theorem for a first order linear-time logic. Publ. Inst. Math., Nouv. S’ er. 69(83), 1–7 (2001) · Zbl 1265.03009
[35] Ognjanović, Z., Marković, Z., Rašković, M.: Completeness theorem for a Logic with imprecise and conditional probabilities. Publ. Inst. Math., Nouv. S’ er. 78(92), 35–49 (2005) · Zbl 1144.03019 · doi:10.2298/PIM0578035O
[36] Ognjanović, Z.: Discrete linear-time probabilistic logics: completeness, decidability and complexity. J. Log. Comput. 16(2), 257–285 (2006) · Zbl 1102.03022 · doi:10.1093/logcom/exi077
[37] Ognjanović, Z., Rašković, M., Marković, Z.: Probability Logics. Ognjanović, Z. (ed.) Logic in Computer Science. Mathematical Institute of Serbian Academy of Sciences and Arts, pp. 35–111, ISBN 978-86-80593-40-1 (2009) · Zbl 1224.03005
[38] Ognjanović, Z., Doder, D., Marković, Z.: A branching time logic with two types of probability operators. In: SUM 2011, LNCS 6929, pp. 219–232 (2011)
[39] Perović, A., Ognjanović, Z., Rašković, M., Marković, Z.: A probabilistic logic with polynomial weight formulas. In: FoIKS 2008, pp. 239–252 (2008) · Zbl 1138.03315
[40] Prior, A.: Time and Modality. Clarendon, Oxford (1957) · Zbl 0079.00606
[41] Rašković, M.: Classical logic with some probability operators. Publ. Inst. Math., Nouv. S’ er. 53(67), 1–3 (1993) · Zbl 0799.03018
[42] Rašković, M., Ognjanović, Z.: A first order probability logic, LP Q . Publ. Inst. Math., Nouv. S’ er. 65(79), 1–7 (1999) · Zbl 1006.03018
[43] Rašković, M., Marković, Z., Ognjanović, Z.: A logic with approximate conditional probabilities that can model default reasoning. Int. J. Approx. Reason. 49(1), 52–66 (2008) · Zbl 1184.68520 · doi:10.1016/j.ijar.2007.08.006
[44] Reynolds, M.: An axiomatization of full computation tree logic. J. Symb. Log. 66(3), 1011–1057 (2001) · Zbl 1002.03015 · doi:10.2307/2695091
[45] Shafer, G.: A Mathematical Theory of Evidence. Princeton University Press, Princeton, NJ (1976) · Zbl 0359.62002
[46] Shafer, G.: Belief functions and parametric models (with commentary). J. R. Stat. Soc., Ser. B. 44, 322–352 (1982) · Zbl 0499.62007
[47] Stirling, C.: Modal and temporal logic. In: Handbook of Logic in Computer Science, vol. 2, pp. 477–563 (1992)
[48] van Benthem, J.: The Logic of Time. Springer, Berlin Heidelberg New York (1991) · Zbl 0758.03012
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.