Home

Research team

Current graduate students

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

Recent journal articles

  1. J. Pachl and P. Sánchez Terraf, “Semipullbacks of labelled Markov processes,” arXiv:1706.02801 1706.02801 (2020). To be published in Logical Methods in Computer Science.
    [ arXiv | Abstract | BibTeX ]

    A \emph{labelled Markov process (LMP)} consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP $S$ and $S’$ “behave the same”. There are two natural categorical definitions of sameness of behavior: $S$ and $S’$ are \emph{bisimilar} if there exist an LMP $ T$ and measure preserving maps forming a diagram of the shape $ S\leftarrow T \rightarrow{S’}$; and they are \emph{behaviorally equivalent} if there exist some $ U$ and maps forming a dual diagram $ S\rightarrow U \leftarrow{S’}$. These two notions differ for general measurable spaces but Edalat proved that they coincide for analytic Borel spaces, showing that from every diagram $ S\rightarrow U \leftarrow{S’}$ one can obtain a bisimilarity diagram as above. Moreover, the resulting square of measure preserving maps is commutative (a \emph{semipullback}). In this paper, we extend Edalat’s result to measurable spaces $S$ isomorphic to a universally measurable subset of a Polish space with the trace of the Borel $\sigma$-algebra, using a version of Strassen’s theorem on common extensions of finitely additive measures.

    @article{2017arXiv170602801P,
    author = {Pachl, Jan and S{\'a}nchez Terraf, Pedro},
    title = {Semipullbacks of labelled {M}arkov processes},
    journal = {ArXiv e-prints},
    archiveprefix = {arXiv},
    eprint = {1706.02801},
    volume = {1706.02801},
    primaryclass = {math.PR},
    keywords = {Mathematics - Probability, Computer Science - Logic in Computer Science, 28A35, 28A60, 68Q85, F.4.1, F.1.2},
    year = 2020,
    adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170602801P},
    adsnote = {Provided by the SAO/NASA Astrophysics Data System},
    note = {To be published in Logical Methods in Computer Science},
    abstract = {A \emph{labelled Markov process (LMP)} consists of a measurable
    space $S$ together with an indexed family of Markov kernels from $S$
    to itself. This structure has been used to model probabilistic
    computations in Computer Science, and one of the main problems in
    the area is to define and decide whether two LMP $S$ and $S'$ ``behave
    the same''. There are two natural categorical definitions of
    sameness of behavior: $S$ and $S'$ are \emph{bisimilar}
    if there exist an LMP $ T$ and measure preserving maps
    forming a diagram of the shape
    $ S\leftarrow T \rightarrow{S'}$; and they
    are \emph{behaviorally equivalent}
    if there exist some $ U$ and maps forming a dual diagram
    $ S\rightarrow U \leftarrow{S'}$.
    These two notions differ for general measurable spaces but Edalat
    proved that they coincide for analytic Borel spaces, showing that
    from every
    diagram $ S\rightarrow U \leftarrow{S'}$ one can obtain a
    bisimilarity diagram as above. Moreover, the resulting square of
    measure preserving maps is commutative (a \emph{semipullback}).
    In this paper, we extend Edalat's result to measurable spaces $S$
    isomorphic to a universally measurable subset of
    a Polish space with the trace of the Borel $\sigma$-algebra, using a
    version of Strassen's theorem on
    common extensions of finitely additive measures.}
    }

  2. 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). [DOI]
    [ 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.}
    }

  3. 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}
    }

  4. 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}
    }


Recent conference papers

  1. 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. [DOI]
    [ 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}
    }

  2. 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). [DOI]
    [ 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)}
    }

Sponsors
CIEM-Conicet Conicet ANPCyT Secyt-UNC Argentina