3 papers
cs.LO2026
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…
cs.GT2025
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…
cs.LO2025
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…