Paqui Lucio

Last modified: September 2021

DISCLAIMER: This directory contains postscript files of articles that may be covered by copyright. You may browse the articles at your convenience (in the same spirit as you may read a journal or a proceeding article in a public library). Retrieving, copying, distributing these files may violate the copyright protection law. We recommend that the user abides international law in accessing this directory.

 

Tableaux and Sequent Calculi for  CTL and ECTL: Satisfiability Test with Certifying Proofs and Models

Alex Abuin, Alexander Bolotov, Montserrat Hermo and Paqui Lucio,

To appear in Journal of Logical and Algebraic Methods in Programming.

 

 

Verified Model Checking for Conjunctive Positive Logic.

Alex Abuin. Unai Diaz de Cerio, Montserrat Hermo and Paqui Lucio

SN Computer Science, Volume 2, Article number: 344 (2021), Springer.

doi: 10.1007/s42979-020-00417-3 [PDF][Bibtex]

 

 

One-pass Context-based Tableaux Systems for CTL and ECTL.

Alex Abuin, Alexander Bolotov, Montserrat Hermo and Paqui Lucio,

27th International Symposium on Temporal Representation and Reasoning, TIME 2020. 23-25 September 2020 - Bozen-Bolzano, Italy.

LIPIcs, Vol 178, pages 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany.

doi: 10.4230/LIPIcs.TIME.2020.14 [PDF][Bibtex]

 

 

Branching-Time Logic ECTL# and its Tree-style One-pass Tableau: Extending Fairness Expressibility of ECTL+. 

Alexander Bolotov, Montserrat Hermo, and Paqui Lucio.
Theoretical Computer Science, Volume 813, Pages 428-451, 2020.

doi:10.1016/j.tcs.2020.02.015 [PDF][Bibtex]

A largest version with more detailed proofs is available: Technical Report.

 

 

Towards Certified Model Checking for PLTL using One-pass Tableaux.

Alex Abuin, Alexander Bolotov, Unai Diaz de Cerio, Paqui Lucio, Montserrat Hermo.
26th International Symposium on Temporal Representation and Reasoning, TIME 2019. Malaga, Spain 16 - 19 Oct  2019

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany.

doi:10.4230/LIPIcs.TIME.2019.12 [PDF] [BibTex]

 

 

Using Contexts in Tableaux for PLTL: An illustrative Example.

Alex Abuin, Alexander Bolotov, Unai Diaz de Cerio, Paqui Lucio, Montserrat Hermo.
Proccedings of Automated Reasoning Workshop 2019, London, 2th - 3th September 2019.

https://www.arw2019.org/arw2019-proc.pdf

 

 

Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach (Extended Abstract). 

Alexander Bolotov, Montserrat Hermo and Paqui Lucio,
Actas de las XIX Jornadas sobre Programación y Lenguajes (PROLE 2019), Cáceres, 2-4 September 2019.

[Electronic Edition]

 

 

Automatic white-box testing of first-order logic ontologies.

Javier Álvez, Montserrat Hermo, Paqui Lucio and German Rigau.

Journal of Logic and Computation, Volume 29, Issue 5, Pages 723–751, September 2019.  

doi: 10.1093/logcom/exz001

Also avalaible at https://arxiv.org/abs/1705.10219v3.

[BibTex]

 

A Framework for the Evaluation of SUMO-based Ontologies Using WordNet.
Javier Álvez, Paqui Lucio and German Rigau.
IEEE Access. Vol. 7, pp 36075-36093, March 2019.
doi: 10.1109/ACCESS.2019.2904835
[BibTex]

 

Extending fairness expressibility of  ECTL+: a tree-style one-pass tableau approach.

Alexander Bolotov, Montserrat Hermo, and Paqui Lucio.

In N. Alechina and K. Norvag and W. Penczek (eds.) 25th International Symposium on Temporal Representation and Reasoning (TIME 2018),
Leibniz International Proceedings in Informatics (LIPIcs), Vol. 120, 5:1-5:22, 2018
doi = 10.4230/LIPIcs.TIME.2018.5  Technical Report

[BibTeX]

 

 

Context-based Model Checking using SMT-solvers.
Alex Abuin, Unai Díaz de Cerio, Montserrat Hermo and Paqui Lucio

In Y. Ortega Mallén (ed.): Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), Sevilla,  Septiembre 2018.

[Electronic Edition]

 

 

Towards the Automatic Verification of QCSP Tractability Results.

Alex Abuin, Hubie Chen, Montserrat Hermo, and Paqui Lucio

In:  Actas de las XVII Jornadas sobre Programación y Lenguajes (PROLE 2017), Tenerife, Julio 2017.

[Electronic Edition]

 

 

Evaluating Automated Theorem Provers Using Adimen-SUMO.

Javier Álvez,  and German Rigau.

In: Laura Kovacs and Andrei Voronkov (eds). Vampire 2016. Proceedings of the 3rd Vampire Workshop,

vol. 44, pages 74--82, Coimbra, Portugal, July 2, 2016.

[BibTeX] [Electronic Edition]

 

 

A Tutorial on Using Dafny to Construct Verified Software.

In Alicia Villanueva (ed): Proceedings XVI Jornadas sobre Programación y Lenguajes (PROLE 2016),

Salamanca, Spain, 14-16th September 2016.

Electronic Proceedings in Theoretical Computer Science 237, pp. 1–19, 11th January 2017.

doi:10.4204/EPTCS.237.1

[BibTeX] [Electronic Edition]

 

 

Evaluating the Competency of a First-Order Ontology.
Javier Álvez,  and German Rigau.

Proceedings of the 8th International Conference on Knowledge Capture (K-CAP 2015) Article No. 28, pp 28:1--28:4,

ACM New York, USA 2015 .

doi: 10.1145/2815833.2816946

[K-CAP-2015-2.pdf] [BibTeX] [Electronic Edition]

 

 

Improving the Competency of First-Order Ontologies.

Javier Álvez,  and German Rigau.

Proceedings of the 8th International Conference on Knowledge Capture (K-CAP 2015) Article No. 15, pp 15:1--15:8,

ACM New York, USA 2015.

doi: 10.1145/2815833.2815841

[K-CAP-2015-1.pdf] [BibTeX] [Electronic Edition]

 

 

An Assertional Proof of the Stability and Correctness of Natural Mergesort.

K. Rustan M. Leino and P. Lucio.

ACM Transactions on Computational Logic, Volume 17 Issue 1, November 2015.

doi: 10.1145/2814571

[acmtocl15.pdf] [BibTeX] [Electronic Edition]

 

 

Projective Quantifier Elimination for Equational Constraint Solving.

Javier Álvez, Montserrat Hermo and Paqui Lucio.

First International Workshop on Quantification --QUANTIFY 2014--

(workshop associated to 2014 Federated Logic Conference), Vienna, Austria, July 2014.

[quantify14.pdf][Electronic Edition]

 

 

Logical Foundations for More Expressive Declarative Temporal Logic Programming Languages.

J. Gaintzarain and P. Lucio,

ACM Transactions on Computational Logic, Volume 14 Issue 4, Article No. 28, pages 28:1--28:41, November 2013.

doi: 10.1145/2528931

[acmtocl13.pdf] [BibTeX] [Electronic Edition]

 

 

Invariant-Free Clausal Temporal Resolution.

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas.

Journal of Automated Reasoning, Volume 50, Issue 1, January 2013.

doi: 10.1007/s10817-011-9241-2

[JAR13.pdf] [BibTeX] [Electronic Edition]

 

 

Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning.

J. Álvez, P. Lucio and G.Rigau.

International Journal on Semantic Web and Information Systems, Volume 8, Issue 4, 2012.

doi: 10.4018/jswis.2012100105

[IJSWIS12.pdf] [BibTeX][Electronic Edition]

 

 

Translating Propositional Extended Conjunctions of Horn Clauses into Boolean Circuits.

M. Hermo, J. Gaintzarain, P. Lucio and M. Navarro.

Theoretical Computer Science  411, 16-18: 1723-1733,  2010.

doi:10.1016/j.tcs.2010.01.013

[TCS10.pdf]  [BibTeX] [Electronic Edition]

 

 

A New Approach to Temporal Logic Programming.

J. Gaintzarain and P. Lucio.
In P. Lucio, G. Moreno, R. Peńa (eds), Actas de las IX Jornadas sobre Programación y Lenguajes,

PROLE’2009, pp 341-350, San Sebastián, Spain, September, 2009.
[prole09.pdf]

 

 

Dual Systems of Tableaux and Sequents for PLTL.

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas.
The Journal of Logic and Algebraic Programming 78: 701–722, 2009.

doi:10.1016/j.jlap.2009.05.001

[JLAP09.pdf]  [BibTeX ] [Electronic Edition]

 

 

A Functorial Framework for Constraint Normal Logic Programming.

P. Lucio, F. Orejas, E. Pasarella and E. Pino,
Applied Categorical Structures 16 (3): 421-450, 2008.
[ACS08.pdf]  [BibTeX ] [Electronic Edition]

 


A Generalization of the Folding Rule for the Clark-Kunen Semantics.
J. Álvez and P. Lucio.

In J. Garrigue and M. Hermenegildo (Eds.): Proceedings of 9th International Symposium,

FLOPS 2008, Ise, Japan, April 14-16, LNCS 4989, pp. 180–194, 2008.

[flops08.pdf] [BibTeX ] [Electronic Edition]

Extended Version available as Technical Report  [UPV-EHU/LSI/TR 01-2008.pdf]

 

 

A New Proposal Of Quasi-Solved Form For Equality Constraint Solving.

Javier Álvez and Paqui Lucio.

Electr. Notes Theor. Comput. Sci. 206: 23-40, 2008.

[prole08a.pdf] [BibTeX] [Electronic Edition]

 

 

Systematic Semantic Tableaux for PLTL.

Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, and Marisa Navarro.

Electr. Notes Theor. Comput. Sci. 206: 59-73, 2008.

DOI: 10.1016/j.entcs.2008.03.075

[prole08b.pdf] [BibTeX] [Electronic Edition]

 

 

A Cut-Free and Invariant-Free Sequent Calculus for PLTL.
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F.Orejas.
In J. Duparc and T.A. Henzinger (Eds.): Computer Science Logic : 21 International Workshop, CSL 2007,

16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, LNCS 4646, pp. 481–495, 2007.
Springer-Verlag Berlin Heidelberg, 2007.
[csl07.pdf] [BibTeX ] [Electronic Edition]

 

 

A functorial framework for constraint normal logic programming.

P. Lucio, F. Orejas, E. Pasarella and E. Pino.

In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer (Eds),  Algebra, Meaning and Computation: Essays dedicated to Joseph A. Goguen

on the Occasion of His 65th Birthday,  LNCS 4060, pp. 555-577, Springer-Verlag,  2006.

[festschrift.pdf]  [BibTeX ] [Electronic Edition]

 

 

Equational Constraint Solving Via a Restricted Form of Universal Quantification.

J. Alvez and P. Lucio.

In J. Dix and S. J. Hegner (Eds.):  Foundations of Information and Knowledge Systems (FoIKS 2006), LNCS 3861, pp. 2–21,

Springer-Verlag Berlin Heidelberg, 2006.

[FoIKS06.pdf]   [BibTeX ]   [Electronic Edition]

 

 

An Algorithm  for Local Variable Elimination in Normal Logic Programs.

J. Alvez and P. Lucio.

15th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2005), London, UK, September 7-9, 2005.

Revised Selected Paper

In Patricia M. Hill (ed.): Logic Based Program Synthesis and Transformation: 15th International Symposium LOPSTR 2005, 

Revised Selected Papers, LNCS 3901, pp. 61 - 79, 2006.

[LOPSTR05.pdf]   [BibTeX ]   [Electronic Edition]

 

 

Elimination of Local Variables from Definite Logic Programs.

J. Alvez and P. Lucio.

IV Jornadas sobre Programación y Lenguajes PROLE 2004, Málaga, Spain 10-12 Noviembre, 2004.

Revised Selected Paper

In S. Lucas (ed.):  Proceedings of the Fourth Spanish Conference on Programming and Computer Languages PROLE 2004,

ENTCS 137 (1), pp 5-24, (20 July 2005).

[ENTCS05.pdf]   [BibTeX ]   [Electronic Edition]

 

 

Equational Constraint Solving using  Quasi-solved Forms.

J. Alvez and P. Lucio.

In M. Kohlhase (chair): 8th International workshop on Unification (UNIF'04) at IJCAR 2004, Cork, Ireland, July 5, 2004.

[UNIF04.pdf]   [BibTeX ]   [Electronic Edition]

 

 

Constructive Negation by Bottom-up Computation of Literal Answers.

J. Alvez, P. Lucio, F. Orejas, E. Pasarella and E. Pino.

In Proceedings of the 2004 ACM Symposium on Applied Computing, Nicosia (Cyprus), Vol. 2:1468-1475, ACM 2004.

[SAC04.pdf]   [BibTeX ]   [Electronic Edition]

 

 

An Implementation of Constructive Negation.

J. Alvez, P. Lucio, F. Orejas, E. Pasarella and E. Pino.

In R. Peña, A. Herranz, J.J. Moreno (eds.): Segundas Jornadas sobre Programación y Lenguajes Prole 2002, pp 55-104, Noviembre 2002.

[Prole02.pdf]  

 

 

Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic.

P. Lucio.

In H. Kirchner and C. Ringeissen (eds.): Proceedings of the Third International Workshop on Frontiers of Combining Systems,

FroCoS 2000, LNCS 1794, pp. 88-104,  Springer, 2000.

[FroCoS00.pdf]   [BibTeX ]  [Electronic Edition]

 

 

An Algebraic Framework for the Definition of Compositional Semantics of Normal Logic Programs.

P. Lucio, F. Orejas and E. Pino.

Journal of Logic Programming, 40(1): 89-124, 1999.

[JLP99.pdf]   [BibTeX ]   [Electronic Edition]

 

 

A Strong Logic Programming View for Static Embedded Implications.

R. Arruabarrena, P. Lucio and M. Navarro.

In W. Thomas (ed.): Proceedings of the Second International Conference on Foundations of  Software Science and Computation Structures,

FOSSACS'99,  LNCS 1578, pp. 56-72,  Springer-Verlag, 1999.

[FoSSaCS99.pdf]   [BibTeX]  

 

 

A Monotonic Declarative Semantics for Normal Logic Programs.

Paqui Lucio, Fernando Orejas, Elvira Pino.

In Moreno Falaschi, Marisa Navarro, Alberto Policriti (Eds.): Joint Conf. on Declarative Programming, APPIA-GULP-PRODE'97,

Grado, Italy, June 16-19, pp 271-282, 1997.

[LOP97.pdf]   [BibTeX] [Electronic Edition]

 

 

Reasoning with Higher Order Partial Functions.

A. Gavilanes-Franco, P. Lucio-Carrasco, M. Rodriguez-Artalejo.

In E. Börger, G. Jäger, H. K. Büning, S. Martini, M. M. Richter (Eds.): Computer Science Logic, 6th Workshop,

CSL '92, San Miniato, Italy, September 28 - October 2, 1992,

SELECTED PAPERS, Lecture Notes in Computer Science 702:167-181, 1993, Springer-Verlag.

[10.1007/3-540-56992-8_12]  [BibTeX]

 

 

A First Order Logic for Partial Functions.

A. Gavilanes-Franco, F. Lucio-Carrasco.

Theoretical Computer Science, 74(1): 37-69, 1990, Elsevier.

[10.1016/0304-3975(90)90005-3]  [BibTeX]

 

 

A First Order Logic for Partial Functions- Extended Abstract.

F. Lucio-Carrasco and A. Gavilanes-Franco.

In B. Monien, R. Cori (Eds.), STACS '89 Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science,

Lecture Notes in Computer Science 349:47-58, Springer-Verlag,, 1989.

[10.1007/BFb0028972]    [BibTeX]

 

 

Some General Incompleteness Results for Partial Correctness Logic.

M. T. Hortalá-Gonzalez, F. Lucio- Carrasco, M. Rodríguez-Artalejo.

Information and Computation, 79(1): 22-42,  Elsevier, 1988.

[10.1016/0890-5401(88)90015-6]   [BibTeX]