Zobrazeno 41 - 50
of 95
pro vyhledávání: '"Jeremy Avigad"'
Publikováno v:
Interactive Theorem Proving ISBN: 9783319089690
ITP
ITP
We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f19d88ae18be27550fc0c9585e90e56e
http://arxiv.org/abs/1404.4410
http://arxiv.org/abs/1404.4410
Autor:
Jeremy Avigad
Publikováno v:
ACM SIGACT News. 32:15-19
Autor:
Jeremy Avigad
Publikováno v:
The Mathematical Intelligencer. 32:79-81
Autor:
Jeremy Avigad
Publikováno v:
Journal of Philosophy. 96:638-642
Autor:
Jeremy Avigad
Publikováno v:
Archive for Mathematical Logic. 37:235-240
Solovay has shown that if \(\cal{O}\) is an open subset of \(P(\omega)\) with code \(S\) and no infinite set avoids \(\cal{O}\), then there is an infinite set hyperarithmetic in \(S\) that lands in \(\cal{O}\). We provide a direct proof of this theor
Autor:
Jeremy Avigad
Publikováno v:
Annals of Pure and Applied Logic. 92:1-34
In 1958 Godel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Godel's T to theories Pn of “predicative” func
Autor:
Jeremy Avigad
Publikováno v:
The Bulletin of Symbolic Logic. 20:500-501
Autor:
Jeremy Avigad, Richard Sommer
Publikováno v:
Bulletin of Symbolic Logic. 3:17-52
We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of num
Autor:
Jeremy Avigad, Iovino, J.
Publikováno v:
Scopus-Elsevier
Given a convergence theorem in analysis, under very general conditions a model-theoretic compactness argument implies that there is a uniform bound on the rate of metastability. We illustrate with three examples from ergodic theory.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1d2c78136b5dbf38eb2b6fbf153c8542
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6a87369de90a2c8255d74809448bd774