7 citations · 7 across the 5 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…