2008 |
27 | EE | Steven Kieffer,
Jeremy Avigad,
Harvey Friedman:
A language for mathematical language management
CoRR abs/0805.1386: (2008) |
2007 |
26 | EE | Jeremy Avigad,
Kevin Donnelly,
David Gray,
Paul Raff:
A formally verified proof of the prime number theorem.
ACM Trans. Comput. Log. 9(1): (2007) |
25 | EE | Jeremy Avigad,
Kevin Donnelly:
A decision procedure for linear "big O" equations
CoRR abs/cs/0701073: (2007) |
24 | EE | Jeremy Avigad,
Kevin Donnelly:
A Decision Procedure for Linear "Big O" Equations.
J. Autom. Reasoning 38(4): 353-373 (2007) |
23 | EE | Jeremy Avigad,
Yimu Yin:
Quantifier elimination for the reals with a predicate for the powers of two.
Theor. Comput. Sci. 370(1-3): 48-59 (2007) |
2006 |
22 | EE | Jeremy Avigad,
Ksenija Simic:
Fundamental notions of analysis in subsystems of second-order arithmetic.
Ann. Pure Appl. Logic 139(1-3): 138-184 (2006) |
21 | EE | Jeremy Avigad,
Harvey Friedman:
Combining decision procedures for the reals
CoRR abs/cs/0601134: (2006) |
20 | EE | Jeremy Avigad,
Yimu Yin:
Quantifier elimination for the reals with a predicate for the powers of two
CoRR abs/cs/0610117: (2006) |
19 | EE | Jeremy Avigad,
Harvey Friedman:
Combining decision procedures for the reals.
Logical Methods in Computer Science 2(4): (2006) |
18 | EE | Jeremy Avigad:
Mathematical Method and Proof.
Synthese 153(1): 105-159 (2006) |
2005 |
17 | EE | Arnold Beckmann,
Jeremy Avigad,
Georg Moser:
Preface.
Ann. Pure Appl. Logic 136(1-2): 1-2 (2005) |
16 | EE | Jeremy Avigad,
Kevin Donnelly,
David Gray,
Paul Raff:
A formally verified proof of the prime number theorem
CoRR abs/cs/0509025: (2005) |
2004 |
15 | EE | Jeremy Avigad,
Kevin Donnelly:
Formalizing O Notation in Isabelle/HOL.
IJCAR 2004: 357-371 |
14 | EE | Jeremy Avigad:
Forcing in proof theory.
Bulletin of Symbolic Logic 10(3): 305-333 (2004) |
2003 |
13 | EE | Jeremy Avigad:
Eliminating definitions and Skolem functions in first-order logic.
ACM Trans. Comput. Log. 4(3): 402-415 (2003) |
12 | EE | Jeremy Avigad:
Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234].
Ann. Pure Appl. Logic 121(2-3): 285- (2003) |
2002 |
11 | | Jeremy Avigad:
Saturated models of universal theories.
Ann. Pure Appl. Logic 118(3): 219-234 (2002) |
10 | EE | Jeremy Avigad:
Update Procedures and the 1-Consistency of Arithmetic.
Math. Log. Q. 48(1): 3-13 (2002) |
2001 |
9 | | Jeremy Avigad:
Eliminating Definitions and Skolem Functions in First-Order Logic.
LICS 2001: 139-146 |
8 | | Jeremy Avigad:
Algebraic proofs of cut elimination.
J. Log. Algebr. Program. 49(1-2): 15-30 (2001) |
2000 |
7 | | Jeremy Avigad:
Interpreting Classical Theories in Constructive Ones.
J. Symb. Log. 65(4): 1785-1812 (2000) |
1999 |
6 | | Jeremy Avigad,
Richard Sommer:
The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength.
J. Symb. Log. 64(1): 327-349 (1999) |
1998 |
5 | | Jeremy Avigad:
Predicative Functionals and an Interpretation of ID<omega.
Ann. Pure Appl. Logic 92(1): 1-34 (1998) |
4 | EE | Jeremy Avigad:
An effective proof that open sets are Ramsey.
Arch. Math. Log. 37(4): 235-240 (1998) |
1997 |
3 | EE | Jeremy Avigad,
Richard Sommer:
A model-theoretic approach to ordinal analysis.
Bulletin of Symbolic Logic 3(1): 17-52 (1997) |
1996 |
2 | | Jeremy Avigad:
Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic.
Ann. Pure Appl. Logic 82(2): 165-191 (1996) |
1 | | Jeremy Avigad:
On the Relationship Between ATR0 and ID<omega.
J. Symb. Log. 61(3): 768-779 (1996) |