Publications

2025

1. TABLEAUX

   Interpolation for Converse Propositional Dynamic Logic

   Johannes Kloibhofer, Francisco Trucco Dalmas, and Yde Venema

   In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025), 2025

   Best Student Paper Abs Bib

   Best Student Paper Award

   Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara’s proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.

   @inproceedings{kloibhofer2025interpolation,
     author = {Kloibhofer, Johannes and Trucco Dalmas, Francisco and Venema, Yde},
     title = {Interpolation for Converse Propositional Dynamic Logic},
     booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025)},
     year = {2025},
     publisher = {Springer},
     url = {https://link.springer.com/chapter/10.1007/978-3-032-06085-3_14},
   }

2. arXiv

   Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof

   Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, and 3 more authors

   2025

   arXiv preprint arXiv:2503.13276

   Abs arXiv Bib

   We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later criticized in the literature or retracted. Our proof is based on the main ideas from Borzechowski (1988). We define a cyclic tableau system for PDL with a loading mechanism to recognize successful repeats. For this system, we show soundness and completeness via a game. To show interpolation, we modify Maehara’s method to work for tableaux with repeats: we first define pre-interpolants at each node, and then use a quasi-tableau to define interpolants for clusters (strongly connected components). In different terms, our method solves the fixpoint equations that characterize the desired interpolants, and the method ensures that the solutions to these equations can be expressed within PDL. The proof is constructive and we show how to compute interpolants. We also make available a Haskell implementation of the proof system that provides interpolants. Lastly, we mention ongoing work to formally verify this proof in the interactive theorem prover Lean, and several questions for future work.

   @unpublished{borzechowski2025pdlcraig,
     author = {Borzechowski, Manfred and Gattinger, Malvin and Hvid Hansen, Helle and Ramanayake, Revantha and Trucco Dalmas, Francisco and Venema, Yde},
     title = {Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof},
     year = {2025},
     note = {arXiv preprint arXiv:2503.13276},
     url = {https://arxiv.org/abs/2503.13276},
   }

2019

1. DALI

   Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq

   Raul Fervari, Francisco Trucco, and Beta Ziliani

   In Dynamic Logic: New Trends and Applications (DALI 2019), 2019

   Abs Bib

   Over the last years, the study of logics that can modify a model while evaluating a formula has gained in interest. Motivated by many examples in practice such as hybrid logics, separation logics and dynamic epistemic logics, the ability of updating a model has been investigated from a more general point of view. In this work, we formalize and verify in the proof assistant Coq, the bisimulation theorems for a particular family of dynamic logics that can change the accessibility relation of a model. The benefits of this formalization are twofold. First, our results apply for a wide variety of dynamic logics. Second, we argue that this is the first step towards the development of a modal logic library in Coq, which allows us to mechanize many relevant results in modal logics.

   @inproceedings{fervari2019mechanizing,
     author = {Fervari, Raul and Trucco, Francisco and Ziliani, Beta},
     title = {Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq},
     booktitle = {Dynamic Logic: New Trends and Applications (DALI 2019)},
     year = {2019},
     url = {https://link.springer.com/chapter/10.1007/978-3-030-38808-9_1},
   }

2018

1. Acta Tropica

   Modeling Dengue vector population using remotely sensed data and machine learning

   Juan M. Scavuzzo, Francisco Trucco, Manuel Espinosa, and 4 more authors

   Acta Tropica, 2018

   Abs Bib

   Mosquitoes are vectors of many human diseases. In particular, Aedes ægypti (Linnaeus) is the main vector for Chikungunya, Dengue, and Zika viruses in Latin America and it represents a global threat. Public health policies that aim at combating this vector require dependable and timely information, which is usually expensive to obtain with field campaigns. For this reason, several efforts have been done to use remote sensing due to its reduced cost. The present work includes the temporal modeling of the oviposition activity (measured weekly on 50 ovitraps in a north Argentinean city) of Aedes ægypti (Linnaeus), based on time series of data extracted from operational earth observation satellite images. We use are NDVI, NDWI, LST night, LST day and TRMM-GPM rain from 2012 to 2016 as predictive variables. In contrast to previous works which use linear models, we employ Machine Learning techniques using completely accessible open source toolkits. These models have the advantages of being non-parametric and capable of describing nonlinear relationships between variables. Specifically, in addition to two linear approaches, we assess a support vector machine, an artificial neural networks, a K-nearest neighbors and a decision tree regressor. Considerations are made on parameter tuning and the validation and training approach. The results are compared to linear models used in previous works with similar data sets for generating temporal predictive models. These new tools perform better than linear approaches, in particular nearest neighbor regression (KNNR) performs the best. These results provide better alternatives to be implemented operatively on the Argentine geospatial risk system that is running since 2012.

   @article{scavuzzo2018modeling,
     author = {Scavuzzo, Juan M. and Trucco, Francisco and Espinosa, Manuel and Tauro, Carolina B. and Abril, Marcelo and Scavuzzo, Carlos M. and Frery, Alejandro C.},
     title = {Modeling Dengue vector population using remotely sensed data and machine learning},
     journal = {Acta Tropica},
     year = {2018},
     publisher = {Elsevier},
     url = {https://doi.org/10.1016/j.actatropica.2018.05.003},
   }