Fairness in Theorem Proving

Fairness is a fundamental concept that arises in many aspects of computing. In theorem proving a refutationally complete inference system is complemented with a fair search plan, or strategy, to obtain a complete theorem-proving method. Although in practice we often give up on completeness, we usually do so by deliberately weakening a complete method, so that the practical interest in incomplete methods does not diminish the importance of fairness. While many refutationally complete non-trivial inference systems are known, the design of fair search plans that are not trivial and unfair search plans that are useful is a challenge. In this talk we discuss various notions of fairness for different theorem-proving paradigms. We analyze the connection between fairness and redundancy, how both are defined in terms of orderings, how these can be formula orderings or proof orderings. The latter allow us to distinguish between fairness, which yields completeness, and uniform fairness, which yields saturation, suggesting that saturation is too strong for theorem proving.

Speaker Bios

Maria Paola Bonacina is Professor of Computer Science with the Dipartimento di Informatica of the Università degli Studi di Verona. Formerly she was first Assistant Professor and then Associate Professor with the Department of Computer Science of the University of Iowa. While at the University of Iowa she received the NSF CAREER Award and a Dean Scholar Award by the College of Liberal Arts and Sciences. Her research area is artificial intelligence where she works in theorem proving applied to the analysis, verification and synthesis of systems. Her research has been funded by the NSF in the US, by the EU Commission and the Italian Ministry for Education and Research in Italy. At the Università degli Studi di Verona she was Director of Computer Science studies, Chair of the University Evaluation Committee for Computer Science and Mathematics, Dean of the Graduate School of Sciences Engineering Medicine, and Executive Associate Dean of the College of Sciences. Currently, she serves in the Academic Senate as representative of the area of Sciences and Engineering. At the University of Iowa she was elected to the Faculty Assembly of the College of Liberal Arts and Sciences, and to the Faculty Hiring Committee whenever her Department had an opening. At the international level, she was elected twice to the Board of Trustees of CADE Inc. (Conference on Automated Deduction), both times resulting first with the Single Transferrable Vote system. She served as President of the Board of Trustees of CADE and as one of the Directors of the Association for Automated Reasoning. She is Program Chair of the Twenty-Fourth edition of CADE in 2013. Maria Paola received a Laurea and a Dottorato di Ricerca from the Università degli Studi di Milano, and a PhD from the State University of New York at Stony Brook.