A logic to reason about likelihood (Q1090326)

The modal system LL considered here has S4-necessity G, T-possibility L and axioms and rules for these connectives as well as implication Gp\(\to \sim L\sim p\) (G is stronger than L). Yet another modal connetive \(L^*\) (iteration of L) is characterised by the axiom \(L^*p\leftrightarrow p\vee LL^*p\) and the rule (\(\sim p\to \sim Lp)/\sim p\to \sim L^*p\). Completeness proof and exponential decision algorithm (for the language without \(L^*)\) are given along the familiar lines. L is interpreted as likelihood and it is claimed that the logic might be used in areas such as medical diagnosis where decision making in the presence of uncertainties is crucial. A lot of place is devoted to the proof in the LL of correctness of some aspects of a protocol for exchanging secrets.