Probabilistic Logics are formal languages designed to express properties of probabilistic programs. For most probabilistic logics several key problems are still open. One of such problems is to design convenient analytical proof systems in the style
of Gentzen sequent calculus. This is practically important in order to simplify the task of proof search: the CUT-elimination theorem greatly reduces the search space. In this talk I will present some recent developments in this direction. | 
