@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}
}
@misc{elecccion_definible_cubo,
title = {Una aplicación de selectores definibles a los procesos de decisión de {Markov}},
author = {S{\'a}nchez Terraf, Pedro},
year = 2024,
url = {preprints/eleccion_definible_cubo_2024.pdf},
note = {In Spanish / en español},
keywords = {procesos de decisión de Markov, Teorema de Kuratowski y Ryll-Nardzewski},
year = 2024,
month = oct,
abstract = {En este trabajo pasamos revista al uso, en Ciencias de la Computación, de los
procesos de decisión de Markov sobre espacios de Borel estándares (i.e., que
provienen de espacios separables y completamente metrizables). Mostramos cómo
el Teorema de Selección de Kuratowski y Ryll-Nardzewski se utiliza para
demostrar la existencia de “planificadores” (\textit{schedulers})
medibles Borel. Estos permiten dar una representación determinista de sistemas
que admiten comportamientos probabilistas diversos para cada estado en el
que se encuentran.}
}
This file was generated by bibtex2html 1.99.