David E. Narvaez: Separating and Collapsing Electoral Control Types, More Formally

Abstract: In computational social choice, electoral control refers to attacking elections by adding, deleting, or partitioning voters or candidates. In Carleton et al. (2024) we showed that certain control types that have been traditionally studied in computational social choice are in fact the same problem. This was based on an observation by Hemaspaandra, Hemaspaandra and Menton (2020) who showed “collapses” between several pairs of control types. Carleton et al. then investigated whether any such collapses exist among any other pair of control types. This naturally led to a massive undertake in terms of cases to analyze and theorems to prove. Our goal is to formalize the work of Carleton et al. in the HOL4 theorem prover. Our formalization of the hundreds of theorems proved by Carleton et al. seeks to provide a simpler way to grasp the results, in the hope that simplicity will bring new insight to this line of study.