A logic to reason about likelihood

ABSTRACT

We present a logic LL which uses a modal operator L to help capture the notion of likely. Despite the fact that no use is made of numbers, LL can capture many of the properties of likelihood in an intuitively appealing way. Using standard techniques of modal logic, we give a complete axiomatization for LL and show that satisfiability of LL formulas can be decided in exponential time. We discuss how the logic might be used in areas where decision making is crucial, such as management and medical diagnosis, and conclude by using LL to give a formal proof of correctness of a protocol for exchanging secrets.

REFERENCES

• 1: E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
• 2: M. J. Fischer and R. E. Ladner, Propositional Dynamic Logic of Regular Programs, JCSS18:2, 1979, pp. 194-211.
• 3: J. Y. Halpern and D. A. McAllester, Likelihood, Probability, Knowledge, and Time, unpublished manuscript, 1982.
• 4: G. E. Hughes and M. J. Cresswell, An Introduction to Modal Logic, Methuen, London, 1968.
• 5: Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
• 6: Drew McDermott, Nonmonotonic Logic II: Nonmonotonic Modal Theories, Journal of the ACM (JACM), v.29 n.1, p.33-57, Jan. 1982 [doi>10.1145/322290.322293]
• 7: D. V. McDermott and J. Doyle, Nonmonotonic Logic I, Artificial Intelligence13:1,2, 1980, pp. 41-72.
• 8: R. Moore, Reasoning About Knowledge and Action, Ph.D dissertation, MIT, 1979.
• 9: V.R. Pratt, Models of Program Logics, FOCS, 1979, pp. 115-122.
• 10: M.O. Rabin, How to Exchange Secrets by Oblivious Transfer, unpublished manuscript, 1981
• 11: N. Rescher and A. Urquhart, Temporal Logic, Springer-Verlag, 1971.
• 12: G. Shafer, A Mathematical Theory of Evidence, Princeton University Press, 1976.
• 13: P. Szolovits and S. G. Pauker, Categorical and Probabilistic Reasoning in Medical Diagnosis, Artificial Intelligence11, 1978, pp. 115-144.
• 14: A. Tversky and D. Kahneman, Judgement Under Uncertainty: Heuristics and Biases, Science185, 1974, pp. 1124-1131.
• 15: L. A. Zadeh, Fuzzy Sets, Information and Control8, 1965, pp. 338-353.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Modal logic

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Probabilistic computation

General Terms:
Theory, Verification