Goals in the Propositional Horn Language Are Monotone Boolean Circuits. - Joxe Gaintzarain; Montserrat Hermo; Marisa Navarro (MFCS, 2005)

A Cut-Free and Invariant-Free Sequent Calculus for PLTL. - Joxe Gaintzarain; Montserrat Hermo; Paqui Lucio; Marisa Navarro; Fernando Orejas (CSL, 2007)

Systematic Semantic Tableaux for PLTL. - Joxe Gaintzarain; Montserrat Hermo; Paqui Lucio; Marisa Navarro (PROLE, 2007)

Dual Systems of Tableaux and Sequents for PLTL. - Joxe Gaintzarain; Montserrat Hermo; Paqui Lucio; Marisa Navarro; Fernando Orejas (J. Log. Algebraic Methods Program., 2009)

Translating propositional extended conjunctions of Horn clauses into Boolean circuits. - Joxe Gaintzarain; Montserrat Hermo; Paqui Lucio; Marisa Navarro (Theor. Comput. Sci., 2010)

Invariant-Free Deduction Systems for Temporal Logic. - Jose Gaintzarain (Bull. EATCS, 2013)

Invariant-Free Clausal Temporal Resolution. - Jose Gaintzarain; Montserrat Hermo; Paqui Lucio; Marisa Navarro; Fernando Orejas (J. Autom. Reason., 2013)

Logical foundations for more expressive declarative temporal logic programming languages. - Jose Gaintzarain; Paqui Lucio (ACM Trans. Comput. Log., 2013)