@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -c 1=1 /home/pedro/git/private/papers/unpublished.bib}}
@article{2019arXiv190103313G,
author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
title = {{Mechanization of Separation in Generic Extensions}},
journal = {arXiv e-prints},
keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
year = 2019,
month = jan,
archive = {arXiv},
eprint = {1901.03313},
primaryclass = {cs.LO},
adsurl = {https://ui.adsabs.harvard.edu/\#abs/2019arXiv190103313G},
adsnote = {Provided by the SAO/NASA Astrophysics Data System},
abstract = {We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hypotheses in his development of relativization and absoluteness.}
}
@article{Delta_System_Lemma-AFP,
author = {S{\'a}nchez Terraf, Pedro},
title = {Cofinality and the Delta System Lemma},
journal = {Archive of Formal Proofs},
month = dec,
year = 2020,
note = {\url{https://isa-afp.org/entries/Delta_System_Lemma.html},
Formal proof development},
issn = {2150-914x}
}
@article{Independence_CH-AFP,
author = {Emmanuel Gunther and Miguel Pagano and S{\'a}nchez Terraf, Pedro and Mat\'{\i}as Steinberg},
title = {The Independence of the Continuum Hypothesis in {Isabelle/ZF}},
journal = {Archive of Formal Proofs},
month = mar,
year = 2022,
note = {\url{https://isa-afp.org/entries/Independence_CH.html},
Formal proof development},
issn = {2150-914x}
}
@article{Transitive_Models-AFP,
author = {Emmanuel Gunther and Miguel Pagano and S{\'a}nchez Terraf, Pedro and Mat\'{\i}as Steinberg},
title = {Transitive Models of Fragments of {ZFC}},
journal = {Archive of Formal Proofs},
month = mar,
year = 2022,
note = {\url{https://isa-afp.org/entries/Transitive_Models.html},
Formal proof development},
issn = {2150-914x}
}
This file was generated by bibtex2html 1.99.