Résume | Interactions between logic and computer science have been deeply investigated in the last century, but, surprisingly, the study of probabilistic computation was only marginally touched by such fruitful interchanges. The goal of our study is precisely that of start bridging this gap by developing logical systems corresponding to specific aspects of randomized computation and, thus, by generalizing standard achievements to the probabilistic realm. To do so, the key ingredient is the introduction of new, measure-sensitive quantifiers associated with quantitative interpretations.
Specifically, in this talk I will present an extension of classical propositional logic via counting quantifiers, intuitively expressing that a formula is true in a certain portion of its possible interpretations. Beyond admitting a sound and complete proof system, this logic is shown to be related with counting complexity classes. In particular, it is proved that the complexity of deciding the validity of counting formulas in (a special) prenex normal form perfectly matches the corresponding level of the counting hierarchy, a hierarchy of complexity classes introduced by Wagner in 1984/86 as a generalization of Meyer and Stockmeyer's one and able to express the complexity of many natural problems in which counting is involved.
This is joint work with U. Dal Lago and P. Pistone. |