149 citations · 517 across the 29 of their papers we have counts for
10 papers · 1 filter
Certified Knowledge Compilation with Application to Formally Verified Model Counting
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad +1
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when form…
Verified reductions for optimization
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are…
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong +1
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring inform…
Delta-Decidability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence φcontaining only bounded quantifiers, and any pos…
Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including t…
Type inference in mathematics
Jeremy Avigad
In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in whic…