7 citations · 9 across the 6 of their papers we have counts for
6 papers
Implementing Dependent Type Theory Inhabitation and Unification
Chase Norman, Jeremy Avigad
Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synth…
Stable Voting and the Splitting of Cycles
Wesley H. Holliday, Milan Mossé, Chase Norman +2
Algorithms for resolving majority cycles in preference aggregation have been studied extensively in computational social choice. Several sophisticated cycle-resolving methods, incl…
Canonical for Automated Theorem Proving in Lean
Chase Norman, Jeremy Avigad
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to…
Program Synthesis in Saturation
Petra Hozzová, Laura Kovács, Chase Norman +1
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-ord…
Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting
Wesley H. Holliday, Chase Norman, Eric Pacuit +1
A fundamental principle of individual rational choice is Sen's axiom, also known as expansion consistency, stating that any alternative chosen from each of two menus must be ch…
Voting Theory in the Lean Theorem Prover
Wesley H. Holliday, Chase Norman, Eric Pacuit
There is a long tradition of fruitful interaction between logic and social choice theory. In recent years, much of this interaction has focused on computer-aided methods such as SA…