## Research team

- Diego Vaggione (Head of the group and Full Professor)
- Hector Gramaglia (Associate Professor)
- Miguel Campercholi (Adjunct Professor and Conicet Researcher)
- Pedro Sánchez Terraf (Associate Professor and Conicet Researcher)
- Mariana Badano (Assistant Professor and Postdoctoral fellow)

## Current graduate students

- Guillermo Incatasciato
- Ignacio Made
- Martín Moroni
- Mauricio Tellechea (Assistant Professor)
- Pablo Ventura
- Gonzalo Zigarán

## Recent journal articles

- M. Campercholi, M. Tellechea, and P. Ventura, “Deciding Quantifier-free Definability in Finite Algebraic Structures,” Electronic Notes in Theoretical Computer Science 348: 23-41 (2020). 14th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2019).

[ Download PDF | Abstract | BibTeX ]

This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We show the problem to be coNP-complete and present a decision algorithm based on a semantical characterization of definable relations as those preserved by isomorphisms of substructures. Our approach also includes the design of an algorithm that computes the isomorphism type of a tuple in a finite algebraic structure. Proofs of soundness and completeness of the algorithms are presented, as well as empirical tests assessing their performances.

`@article{CAMPERCHOLI202023, title = {Deciding Quantifier-free Definability in Finite Algebraic Structures}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {348}, pages = {23 - 41}, year = {2020}, note = {14th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2019)}, issn = {1571-0661}, doi = {https://doi.org/10.1016/j.entcs.2020.02.003}, url = {http://www.sciencedirect.com/science/article/pii/S1571066120300037}, author = {Miguel Campercholi and Mauricio Tellechea and Pablo Ventura}, keywords = {Definability, logic, decision algorithm, complexity}, abstract = {This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We show the problem to be coNP-complete and present a decision algorithm based on a semantical characterization of definable relations as those preserved by isomorphisms of substructures. Our approach also includes the design of an algorithm that computes the isomorphism type of a tuple in a finite algebraic structure. Proofs of soundness and completeness of the algorithms are presented, as well as empirical tests assessing their performances.} }`

- D. Vaggione, “Baker-Pixley theorem for algebras in relatively congruence distributive quasivarieties.,” Int. J. Algebra Comput. 29 (3) p. 459–480 (2019). Zbl 1428.08002

[ BibTeX ]`@article{zbMATH07062402, author = {D. {Vaggione}}, title = {{Baker-Pixley theorem for algebras in relatively congruence distributive quasivarieties.}}, fjournal = {{International Journal of Algebra and Computation}}, journal = {{Int. J. Algebra Comput.}}, issn = {0218-1967; 1793-6500/e}, volume = {29}, number = {3}, pages = {459--480}, year = {2019}, publisher = {World Scientific, Singapore}, language = {English}, msc2010 = {08A40 03C40 08B10 08C15}, zbl = {1428.08002} }`

- C. Areces, M. Campercholi, D. Penazzi, and V. Pablo, “The Complexity of Definability by Open First-Order Formulas,” Logic Journal of the IGPL (2019). en prensa.

[ BibTeX ]`@article{Complejidad_parametrica, author = {Areces, Carlos and Campercholi, Miguel and Penazzi, Daniel and Ventura Pablo}, title = {The Complexity of Definability by Open First-Order Formulas}, journal = {Logic Journal of the IGPL}, year = {2019}, note = {en prensa} }`

- D. J. Vaggione, “Infinitary Baker-Pixley theorem.,” Algebra Univers. 79 (3) p. 14 (2018). Id/No 67.

[ BibTeX ]`@article{zbMATH06968526, author = {Diego J. {Vaggione}}, title = {{Infinitary Baker-Pixley theorem.}}, fjournal = {{Algebra Universalis}}, journal = {{Algebra Univers.}}, issn = {0002-5240; 1420-8911/e}, volume = {79}, number = {3}, pages = {14}, note = {Id/No 67}, year = {2018}, publisher = {Springer (Birkh\"auser), Basel; University of Manitoba, Department of Mathematics, Winnipeg}, language = {English}, msc2010 = {08A40 03C40 03C05 08B10} }`

## Recent conference papers

- E. Gunther, M. Pagano, and P. Sánchez Terraf, “Formalization of Forcing in Isabelle/ZF,” in Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, 2020, p. 221–235.

[ Abstract | BibTeX ]

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized Paulson’s ZF-Constructibility library.

`@inproceedings{2020arXiv200109715G, author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro}, title = {{Formalization of Forcing in Isabelle/ZF}}, isbn = {978-3-662-45488-6}, booktitle = {Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1--4, 2020, Proceedings, Part II}, volume = 12167, series = {Lecture Notes in Artificial Intelligence}, editor = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica}, publisher = {Springer International Publishing}, doi = {10.1007/978-3-030-51054-1}, pages = {221--235}, journal = {arXiv e-prints}, keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1}, year = 2020, eid = {arXiv:2001.09715}, archiveprefix = {arXiv}, eprint = {2001.09715}, primaryclass = {cs.LO}, adsurl = {https://ui.adsabs.harvard.edu/abs/2020arXiv200109715G}, abstract = {We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized Paulson's ZF-Constructibility library.}, adsnote = {Provided by the SAO/NASA Astrophysics Data System} }`

- E. Gunther, M. Pagano, and P. Sánchez Terraf, “First steps towards a formalization of Forcing,” Electronic Notes in Theoretical Computer Science 344: 119-136 (2019). The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18).

[ Download PDF | Abstract | BibTeX ]

We lay the ground for an Isabelle/ZF formalization of Cohen’s technique of \emph{forcing}. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does.

`@article{2018arXiv180705174G, author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro}, title = {{First steps towards a formalization of Forcing}}, journal = {Electronic Notes in Theoretical Computer Science}, archiveprefix = {arXiv}, eprint = {1807.05174}, primaryclass = {cs.LO}, keywords = {Computer Science - Logic in Computer Science, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1}, month = jul, adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180705174G}, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, abstract = {We lay the ground for an Isabelle/ZF formalization of Cohen's technique of \emph{forcing}. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does.}, volume = {344}, pages = {119 - 136}, year = {2019}, issn = {1571-0661}, doi = {10.1016/j.entcs.2019.07.008}, url = {http://www.sciencedirect.com/science/article/pii/S157106611930026X}, note = {The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18)} }`