| 2023 | FM | Tableaux for Realizability of Safety Specifications. | Montserrat Hermo, Paqui Lucio, Csar Snchez |
| 2020 | TIME | One-Pass Context-Based Tableaux Systems for CTL and ECTL. | Alex Abuin, Alexander Bolotov, Montserrat Hermo, Paqui Lucio |
| 2019 | TIME | Towards Certified Model Checking for PLTL Using One-Pass Tableaux. | Alex Abuin, Alexander Bolotov, Unai Daz-de-Cerio, Montserrat Hermo, Paqui Lucio |
| 2018 | TIME | Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach. | Alexander Bolotov, Montserrat Hermo, Paqui Lucio |
| 2016 | CADE | Evaluating Automated Theorem Provers Using Adimen-SUMO. | Javier lvez, Paqui Lucio, German Rigau |
| 2008 | FLOPS | A Generalization of the Folding Rule for the Clark-Kunen Semantics. | Javier lvez, Paqui Lucio |
| 2007 | CSL | A Cut-Free and Invariant-Free Sequent Calculus for PLTL. | Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, Fernando Orejas |
| 2005 | LOPSTR | An Algorithm for Local Variable Elimination in Normal Logic Programs. | Javier lvez, Paqui Lucio |
| 2004 | SAC | Constructive negation by bottom-up computation of literal answers. | Javier lvez, Paqui Lucio, Fernando Orejas |
| 1999 | FOSSACS | A Strong Logic Programming View for Static Embedded Implications. | Rosa Arruabarrena, Paqui Lucio, Marisa Navarro |