Publications

Libros

1. José A. Alonso, Joaquín Borrego:
   Agentes inteligentes: una aproximación desde la lógica computacional.
   Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5
2. José A. Alonso, Joaquín Borrego:
   Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos).
   Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7
3. José A. Alonso, Joaquín Borrego, M. Pérez, José L. Ruiz Reina:
   Curso práctico de teoría de conjuntos.
   Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9

Capítulos en libros

1. Gonzalo A. Aranda-Corral, Joaquín Borrego, Antonia M. Chávez
   Ontological dimensions of Semantic Mobile Web 2.0. First principles.
   Handbook of Research on Mobility and Computing: Evolving Technologies and Ubiquitous Impacts; pp. 667-688, 2011.
2. Gonzalo A. Aranda-Corral, Joaquín Borrego, Antonia M. Chávez
   Mereotopological Patterns for Ontology Evolution and Debugging.
   Proceedings of the 3rd Workshop on Computational Topology in Image Context, en IMAGE-A 1(1):151--158 ISSN: 1885-4508, 2010.
3. Francisco J. Martín, L.C. González y R. Serrano
   Sistema experto para el control en tiempo real de procesos de mecanizado.
   Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial ISBN: 978-84-692-6424-9; pp. 477-496, 2009.
4. José A. Alonso y F.F. Serrano
   Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar.
   Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
5. José A. Alonso, Gonzalo A. Aranda-Corral, Joaquín Borrego
   Sistema certificado de decisión proposicional basado en polinomios. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
6. José A. Alonso y E.S. Barraza
   Algoritmo para resolver k-SAT basado en cláusulas. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
7. Francisco J. Martín, José L. Ruiz Reina y L. Lambán
   Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
8. Francisco J. Martín, José L. Ruiz Reina, J. Rubio y L. Lambán
   Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso.
   IX Jornadas sobre Programación y Lenguajes ISBN: 978-84-692-4600-9; pp. 7-14, 2009.
9. D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, José L. Ruiz Reina, R. Sumners, D. Vroon and M. Wilding.
   Efficient execution in an automated reasoning environment.
   IX Jornadas sobre Programación y Lenguajes ISBN: 978-84-692-4600-9; pp. 181, 2009.
10. Joaquín Borrego, Antonia M. Chávez y José A. Alonso
    Inconsistency, Logic Databases, and Ontologies.
    Handbook of Research on Innovations in Database Technologies and Applications: Current and Future Trends ISBN: 978-1-60566-242-8; pp. 1-124, 2009.Published under the imprint Information Science Reference (formerly Idea Group Reference) [1] (Eds.) Viviana E. Ferraggine, Jorge H. Doorn, and Laura C. Rivero, UNICEN.
11. Joaquín Borrego:
    Inteligencia artificial y la semántica del espacio (virtual). Inclusiva-Net: Redes digitales y espacio físico. Media-Lab, Madrid. En Prensa (2008).
12. José A. Alonso, Gonzalo A. Aranda-Corral , Joaquín Borrego, M. Magdalena Fernández y María J. Hidalgo:
    Extending attribute exploration by means of Boolean derivates.
    Proceedings of the Sixth International Conference on Concept Lattice and their Applications. Olomouc, Czech Republic. Radim Belohlavek, Sergei O. Kuznetsov (Eds). Vol. 1. 2008. Pag. 121-132. ISBN: 978-80-244-2111-7
13. Gonzalo A. Aranda-Corral:
    Tratamiento de la semántica emergente mediante sistemas de agentes basados en conocimiento.
    I Simposio de Doctorado en Web Semántica.(CAEPIA 2007, Salamanca). ISBN:
14. Joaquín Borrego, Antonia M. Chávez, Gonzalo A. Aranda-Corral:
    Learning Services Based on Formal Concept Reasoning.
    IADIS International Conference Intelligent Systems and Agents 2007, (IADIS'07). ISBN: 978-972-8924-39-3.(2007).
15. Joaquín Borrego, Antonia M. Chávez:
    Anomalías en Ontologías Provisionales.
    Actas del VIII Congreso ISKO España. Interdisciplinarity and Transdisciplinarity in the Organization of Scientific Knowledge, (ISKO'07). ISBN: 978-84-9773-333-5.(2007).
16. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Logic Databases and Inconsistency Handling. Encyclopedia of Databases Technologies and Applications.
    Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2
17. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Fusión Automatizada de Ontologías: Aplicación al Razonamiento Espacial Cualitativo.
    Actas del congreso 50 Años de Inteligencia Artificial. Campus Multidisciplinar en Percepción e Inteligencia, (CMPI'06). ISBN:84-689-9561-4.(2006).
18. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Formal Verification of Molecular Computational Models in ACL2: a Case Study.
    CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4
19. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    Generalizing Logic Programs Via Subsumption.
    Eurocast 2003 - Cast and Tools for Complexity in Biological, Physical and Engineering Systems (Extended Abstracts). Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. Vol. 1. 2003. Pag. 185-188. ISBN: 84-688-0820-2
20. Joaquín Borrego, A. Fernández Margarit, M.J. Pérez Jiménez:
    On Sigma-n definability in Arithmetic.
    Philosophical dimensions of Logic and Science, pag 47--56. Kluwer Ac. Press (2003)
21. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Termination in ACL2 Using Multiset Relation.
    Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5
22. José A. Alonso, Joaquín Borrego, Antonia M. Chávez, J.D. Navarro:
    A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.
    IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4
23. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático.
    Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 23-32. ISBN: 84-472-0290-9
24. José A. Alonso, María J. Hidalgo, José L. Ruiz Reina, Francisco J. Martín:
    Formalización del Razonamiento Ecuacional en una Lógica Computacional.
    Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 41-50. ISBN: 84-472-0290-9
25. José A. Alonso, Joaquín Borrego:
    Proximidad entre cláusulas en programación lógica inductiva.
    Actas del Encuentro de Matemáticos Andaluces - Volumen 2: Comunicaciones. Sevilla. Universidad de Sevilla-Fundación el Monte. Vol. 2. 2001. Pag. 33-40. ISBN: 84-472-0290-9
26. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Estrategias para la demostración automática de teoremas.
    Libro de Actas Cinte'00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283
27. José A. Alonso, Joaquín Borrego:
    Interpretación reactiva de sistemas basados en conocimiento.
    Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X
28. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la inteligencia artificial).
    IV Jornades Sobre L'ensenyament Universitari de la Informatica (Jenui 98). Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296. ISBN: 84-922538-3-5
29. J.J. Arrabal, D. Balbontín, José A. Alonso, F.F. Lara, Francisco J. Martín, M.J. Pérez, José L. Ruiz Reina:
    GTI: una herramienta de edición de cursos adaptativos.
    Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2
30. L. Laita, E. Roanes, José A. Alonso, E. Briales:
    Verificación algebraica de SBC Basada en la lógica trievaluada, teoría e implementación.
    I Jornadas Sobre Inteligencia Artificial, Control y Sistemas Expertos. Madrid, España. Servicio de Publicaciones de la Universidad de Alcala. 1996. Pag. 241-255. ISBN: 84-8138-147-0
31. José A. Alonso, A. Fernández, M.J. Pérez:
    Razonamiento automático. lógica formal : orígenes, métodos y aplicaciones.
    Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X
32. J.J. Arrabal, José A. Alonso, A. Fernández, M.J. Pérez:
    Automatización de la aritmética.
    Lenguajes Naturales y Lenguajes Formales X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7

Publicaciones en revistas

1. Gonzalo A. Aranda-Corral, Joaquín Borrego
   Mereotopological Analysis of Formal Concepts in Security Ontologies.
   Advances in Soft Computing 85, pp. 33-40, 2010.
2. Gonzalo A. Aranda-Corral, Joaquín Borrego, A. Jiménez Mavillard
   Social Ontology Documentation for Knowledge Externalization.
   Communications in Computer and Information Science 108, pp 137--148, 2010.
3. Gonzalo A. Aranda-Corral, Joaquín Borrego
   Reconciling Knowledge in Social Tagging Web Services.
   LNAI 6077, pp. 383--390, 2010.
4. I. Medina, F. Palomo, José L. Ruiz Reina:
   A Verified Common Lisp implementation of Buchberger's algorithm in ACL2.
   Journal of Symbolic Computation. Vol. 45(1). 2010. Pag. 96-123
5. Gonzalo A. Aranda-Corral, Joaquín Borrego, M. Lebrón
   Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations.
   Lecture Notes in Artificial Intelligence, LNAI 5625, pp. 45-58, Springer-Verlag Berlin Heideberg 2009.
6. Francisco J. Martín, J. Rubio, José L. Ruiz Reina
   ACL2 verification of simplicial degeneracy programs in the Kenzo system.
   Lecture Notes in Artificial Intelligence, LNAI 5625, pp. 106-121, Springer-Verlag Berlin Heideberg 2009.
7. R. Serrano, L. C. González, Francisco J. Martín
   Architecture for the Optimization of a Machining Process in Real Time through Rule-Based Expert System.
   AIP Conference Proceedings, 1181, pp. 652-661, American Institute of Physics 2009.
8. Joaquín Borrego, Antonia M. Chávez
   Using Cognitive Entropy to Manage Uncertain Concepts in Formal Ontologies.
   URSW 2005-2007 Uncertainty Reasoning form the Semantic Web. Lecture Notes in Artificial Intelligence. P.C.G. da Costa et al. (Eds.): URSW 2005-2007, LNAI 5327, pp. 315-329, 2008. Springer-Verlag Berlin Heideberg 2008.
9. D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, José L. Ruiz Reina, R. Sumners, D. Vroon and M. Wilding.
   Efficient execution in an automated reasoning environment,
   Journal of Functional Programming, Vol. 18, Núm. 01, 2008.
10. Joaquín Borrego, Antonia M. Chávez:
    A Formal Foundation for Knowledge Integration of Deficient Information in the Semantic Web.
    The 10th International Conference on Computer Aided Systems Theory. Lecture Notes in Computer Science. R. Moreno Diaz et al. (Eds.): EUROCAST 2007, LNCS 4739, pp. 305-312, 2007. Springer-Verlag Berlin Heideberg 2007. ISSN: 0302-9743
11. José A. Alonso, Joaquín Borrego, María J. Hidalgo, Francisco J. Martín, José L. Ruiz Reina:
    A Formally Verified Prover for the ALC Description Logic.
    Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150
12. Joaquín Borrego, Antonia M. Chávez:
    Visual Ontology Cleaning: Cognitive Principles and Applicability.
    3th European Semantic Web Conference ESWC'06. Lecture Notes in Computer Science. R. Moreno Diaz et al. (Eds.): , LNCS 4011,The Semantic Web: Research and applications pp. 317-331, 2006. Springer-Verlag Berlin Heideberg 2006. ISBN:0302-9743
13. José L. Ruiz Reina, Francisco J. Martín, José A. Alonso, María J. Hidalgo:
    Formal Correctness of a Quadratic Unification Algorithm.
    Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92
14. José A. Alonso, Joaquín Borrego, Antonia M. Chávez, Francisco J. Martín:
    Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.
    IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52
15. Joaquín Borrego, Antonia M. Chávez:
    Extension of Ontologies Assisted by Automated Reasoning Systems.
    The 10th International Conference on Computer Aided Systems Theory. Lecture Notes in Computer Science. R. Moreno Diaz et al. (Eds.): EUROCAST 2005, LNCS 3643, pp. 247-253, 2005. Springer-Verlag Berlin Heideberg 2005.ISBN:3-540-29002-8
16. Francisco J. Martín, José L. Ruiz Reina, José A. Alonso, María J. Hidalgo:
    Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.
    Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372
17. M. Palomo, José A. Alonso, Francisco J. Martín:
    Rete Algorithm Applied to Robotic Soccer.
    Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576
18. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.
    Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91
19. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Formal Verification of a Generic Framework to Synthesize SAT-Provers.
    Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313
20. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Formal Verification of Molecular Computational Models in ACL2: a Case Study.
    Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353
21. Antonia M. Chávez, Joaquín Borrego, José A. Alonso:
    Ontology Cleaning By Mereotopological Reasoning.
    Proceedings. 2004. Pag. 132-137
22. José A. Alonso, María J. Hidalgo, Francisco J. Martín, José L. Ruiz Reina:
    Verification of the Formal Concept Analysis.
    RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16
23. I. Medina, F. Palomo, José A. Alonso, José L. Ruiz Reina:
    Verified Computer Algebra in ACL2 (Grobner Bases Computation).
    Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184
24. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    A Formal Proof of Dickson's Lemma in ACL2.
    Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58
25. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    Generalizing Logic Programs Via Subsumption.
    Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126
26. José A. Alonso, Joaquín Borrego, Antonia M. Chávez, Miguel A. Gutiérrez, J.D. Navarro:
    Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases.
    Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798
27. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.
    Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198
28. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    A Quasi-Metric for Machine Learning.
    Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203
29. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Formal Proofs About Rewriting Using ACL2.
    Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262
30. I. Medina, F. Palomo, José A. Alonso:
    A Certified Polynomial-Based Decision Procedure for Propositional Logic.
    Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312
31. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Formalizing Rewriting in the ACL2 Theorem Prover.
    Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106
32. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Verifying an Applicative ATP Using Multiset Relations.
    Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626
33. J. Chazarain, A. Riscos, José A. Alonso, E. Briales:
    Multivalued-Logic and Gröbner Bases With Applications to Modal Logic.
    Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194

Libros de actas

1. Francisco J. Martín:
   CLAI 2009: Workshop on Computational Logics and Artificial Intelligence.
   Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla. 2009
2. José A. Alonso, José L. Ruiz Reina, Joaquín Borrego, M. Ojeda:
   IDEIA 2002: I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial.
   Sevilla. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002

Aportaciones a congresos

1. Francisco J. Martín, L.C. González y R. Serrano
   Sistema experto para el control en tiempo real de procesos de mecanizado.
   XIII Conferencia de la Asociación Española para la Inteligencia Artificial (CAEPIA-TTIA 2009), Sevilla, 2009.
2. E. S. Barraza, José A. Alonso:
   Algoritmo para resolver k-SAT basado en cláusulas.
   Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
3. José A. Alonso, Gonzalo A. Aranda-Corral, Joaquín Borrego:
   Sistema certificado de decisión proposicional basado en polinomios.
   Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
4. José A. Alonso, F. F. Serrano:
   Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar.
   Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
5. Francisco J. Martín, José L. Ruiz Reina, L. Lambán:
   Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2.
   Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
6. Francisco J. Martín, José L. Ruiz Reina, J. Rubio, L. Lambán:
   Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso.
   IX Jornadas sobre Programación y Lenguajes, (PROLE 2009), San Sebastián, 2009.
7. D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, José L. Ruiz Reina, R. Sumners, D. Vroon and M. Wilding.
   Efficient execution in an automated reasoning environment
   IX Jornadas sobre Programación y Lenguajes, (PROLE 2009), San Sebastián, 2009.
8. Gonzalo A. Aranda-Corral, Joaquín Borrego, M. Lebrón:
   Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations.
   16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, (CALCULEMUS'09), Ontario (Canadá), 2009.
9. Francisco J. Martín, J. Rubio, José L. Ruiz Reina:
   ACL2 verification of simplicial degeneracy programs in the Kenzo system.
   16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, (CALCULEMUS'09), Ontario (Canadá), 2009.
10. R. Serrano, L.C. González, Francisco J. Martín:
    Arquitectura para la optimización de un proceso de mecanizado en tiempo real mediante un sistema experto, Third Manufacturing Engineering Society International Conference, (MESIC-09), Alcoy, 2009.
11. Antonio Jiménez Mavillard, Gonzalo A. Aranda-Corral, Joaquín Borrego:
    Una herramienta para la documentación colaborativa de ontologías.
    Conferencia Internacional de Software Libre 2008 (OSWC 2008).
12. Joaquín Borrego, Antonia M. Chávez, Gonzalo A. Aranda-Corral:
    Learning Services Based on Formal Concept Reasoning.
    IADIS International Conference Intelligent Systems and Agents 2007, (IADIS'07). ISBN: 978-972-8924-39-3.(2007).
13. Joaquín Borrego, Antonia M. Chávez:
    Anomalías en Ontologías Provisionales.
    Actas del VIII Congreso ISKO España. Interdisciplinarity and Transdisciplinarity in the Organization of Scientific Knowledge, (ISKO'07). ISBN: 978-84-9773-333-5.(2007).
14. M. Andres, L. Lamban, J. Rubio, José L. Ruiz Reina:
    Formalizing Simplicial Topology in ACL2.
    Seventh International Workshop on the ACL2 Theorem Prover and its Application, Austin, Texas (Estados Unidos), 2007.
15. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Fusión Automatizada de Ontologías: Aplicación al Razonamiento Espacial Cualitativo.
    Actas del congreso 50 Años de Inteligencia Artificial. Campus Multidisciplinar en Percepción e Inteligencia, (CMPI'06). ISBN:84-689-9561-4.(2006).
16. Joaquín Borrego, Antonia M. Chávez:
    Controlling Ontology Extension by Uncertain Concepts through Cognitive Entropy.
    4th International Semantic Web Conference, Workshop on Uncertainty Reasoning for the Semantic Web. Noviembre 2005. Galway, Irlanda.
17. José A. Alonso, María J. Hidalgo, Francisco J. Martín, José L. Ruiz Reina:
    A Formally Verified Proof (in PVS) of the Strong Completeness Theorem of Propositional SLD-Resolution.
    Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 83-86
18. Francisco J. Martín, José L. Ruiz Reina, José A. Alonso, María J. Hidalgo:
    Proof Pearl: a Formal Proof of Higman's Lemma in ACL2.
    Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics (18). Num. 18. Oxford, Reino Unido. Springer-Verlag. 2005. Pag. 358-372. ISBN: 3-540-28372-2
19. M. Palomo, Francisco J. Martín, José A. Alonso:
    Rete Algorithm Applied to Robotic Soccer.
    Cast and Tools for Robotics, Vehicular and Communication Systems. Computer Aided Systems Theory, Eurocast 2005 (10). Num. 10. Las Palmas de Gran Canaria, España. Actas del Congreso. 2005. Pag. 280-283
20. José L. Ruiz Reina, Francisco J. Martín, José A. Alonso, María J. Hidalgo:
    A Formally Verified Quadratic Unification Algorithm.
    Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2004). Austin, Texas, EEUU. University of Austin. 2004. Pag. 1-32
21. José A. Alonso, Joaquín Borrego:
    Generalizing Logic Programs Via Subsumption.
    Computer Aided System Theory - Eurocast 2003: 9th International Workshop on Computer Aided Systems Theory [recurso Electrónico]. International Workshop on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Springer-Verlag. 2004. Pag. 115-126. ISBN: 3-540-20221-8
22. Antonia M. Chávez, José A. Alonso, Joaquín Borrego:
    Ontology Cleaning By Mereotopological Reasoning.
    Database and Expert Systems Applications. Webs 2004. International Workshop on Web Semantics. Webs 2004. (Dexa 2004) (3). Num. 3. Zaragoza, España. IEEE Press. 2004. Pag. 132-137
23. José A. Alonso, Joaquín Borrego, Antonia M. Chávez:
    Towards a Tool for Ontology Engineering.
    World Automation Congress: Advances in Robotics, Manufacturing, Automation, Control, Soft Computing, Multimedia, Biomedicine, Image Processing and Financial Engineering. Vol. IV. World Automation Congress. Sevilla, Spain. Tsi Press. 2004. Pag. 1-100. ISBN: 1-889335-20-7
24. I. Medina, F. Palomo, José A. Alonso, José L. Ruiz Reina:
    Verified Computer Algebra in ACL2 (Gröbner Basis Computation).
    Proceedings of the 7th Int. Conference on Artificial Intelligence and Symbolic Computation (Aisc 2004). 7th Int. Conference on Artificial Intelligence and Symbolic Computation, Aisc 2004. Linz, Austria. Springer-Verlag. 2004. Pag. 171-184
25. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    A Formal Proof of Dickson's Lemma in ACL2.
    Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Almaty, Kazakhstan. Springer-Verlag. 2003. Pag. 49-58
26. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.
    LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. International Workshop on Logic Based Program Synthesis and Transformation (). Uppsala, Suecia. Katholieke Universiteit Leuven, Dep. of Computer Science. 2003. Pag. 97-112
27. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Formal Verification of Molecular Computational Models in ACL2: a Case Study.
    CAEPIA-TTIA 2003. X Conferencia de la Asocicación Española para la Inteligenciia Artificial. Asociación Española para la Inteligencia Artificial. Conferencia. Num. 10. San Sebastián. Universidad del País Vasco, Servicio Editorial. 2003. Pag. 235-240. ISBN: 84-8373-564-4
28. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    Generalizing Logic Programs Via Subsumption.
    Eurocast 2003: Cast and Tools for Complexity in Biological, Physical and Engineering Systems: Extended Abstracts. International Conference on Computer Aided Systems Theory. Num. 9. Las Palmas de Gran Canaria. Universidad de las Palmas de Gran Canaria. 2003. Pag. 185-188. ISBN: 84-688-0820-2
29. Antonia M. Chávez, Joaquín Borrego, José A. Alonso:
    Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases
    (Iea/Aie 2003). Libro de Actas del 16th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Iea/Aie 2003). Iea/Aie 2003 (). Loughborough, United Kingdom. Springer, Berlín, Alemania. 2003. Pag. 789-798
30. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory.
    Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 188-203
31. José A. Alonso, Joaquín Borrego, Antonia M. Chávez, J.D. Navarro:
    A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.
    Proc. of the 28th Annual Conference of IEEE Industrial Electronics Society. The 28th Annual Conference of IEEE Industrial Electronics Society. Sevilla, España. IEEE Press. 2002. Pag. 1806-1811
32. José A. Alonso, Joaquín Borrego:
    A Quasi-Metric for Machine Learning.
    8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203
33. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    A Theory About First-Order Terms in ACL2.
    Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 78-100
34. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Desarrollo Formal y Verificación de Sistemas Proposicionales.
    I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 1-12
35. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Progress Report: Term Dags Using Stobjs.
    Third International Workshop on the ACL2 Theorem Prover and Its Applications. Third International Workshop on the ACL2 Theorem Prover and Its Applications. Num. 3. Grenoble, Francia. Proceedings of the Conference. 2002. Pag. 101-108
36. José A. Alonso, Joaquín Borrego, Antonia M. Chávez, Miguel A. Gutiérrez:
    Towards a Practical Argumentative Reasoning with Qualitative Spatial Database.
    I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 111-120
37. José A. Alonso, Joaquín Borrego, María J. Hidalgo, Francisco J. Martín, José L. Ruiz Reina:
    Una introducción al análisis formal de conceptos en PVS.
    I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 33-46
38. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Verificación formal y eficiencia: un caso de estudio aplicado a la unificación de términos.
    I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Actas del Congreso. 2002. Pag. 77-90
39. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.
    Preproceedings of the International Workshop on Logic Based Program Development and Transformation. International Workshop on Logic Based Program Development and Transformation. Madrid, Spain. Facultad de Informática de la Universidad Politécnica de Madrid. 2002. Pag. 182-197
40. I. Medina, F. Palomo, José A. Alonso:
    A Certified Polynomial-Based Decision Procedure for Propositional Logic.
    International Conference on Theorem Proving in Higher Order Logics. International Conference on Theorem Proving in Higher Order Logics (14). Num. 14. Edimburgo (Escocia), Reino Unido. Division of Informatics of Edinburgh University. 2001. Pag. 297-312
41. José A. Alonso, María J. Hidalgo, Francisco J. Martín, José L. Ruiz Reina:
    Formalización del razonamiento ecuacional en una lógica computacional.
    Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 41-50. ISBN: 84-472-0639-4
42. José A. Alonso, Joaquín Borrego:
    Proximidad entre cláusulas en Programación Lógica Inductiva.
    Actas del I Encuentro de Matemáticos Andaluces. Encuentro de Matemáticos Andaluces. Num. 1. Sevilla, España. Universidad de Sevilla. Secretariado de Publicaciones. 2001. Pag. 33-40. ISBN: 84-472-0639-4
43. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Verifying an Applicative ATP Using Multiset Relations.
    Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626
44. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using ACL2).
    Proceedings of the Third International Workshop on First-Order Theorem Proving. First-Order Theorem Proving (3). Num. 3. ST Andrews, Scotland. Fachberichte Informatik, Universitat Koblenz-Landau. 2000. Pag. 206-216
45. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    A Topological Study of the Upward Refinement Operators on ILP.
    ILP 2000 - Work in Progress Reports. Inductive Logic Programming 10th International Conference, ILP 2000. Londres, Reino Unido. James Cussens - Alan Frisch (Eds.). 2000. Pag. 120-137
46. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Formalizing Rewriting in the ACL2 Theorem Prover.
    Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. Int. Conference on Artificial Intelligence and Symbolic Computation (). Madrid, España. Springer-Verlag. 2000. Pag. 92-106
47. José L. Ruiz Reina, José A. Alonso, María J. Hidalgo, Francisco J. Martín:
    Multiset Relations: a Tool for Proving Termination.
    Proceedings of the ACL2 Workshop 2000. Second ACL2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91
48. Miguel A. Gutiérrez, José A. Alonso, Joaquín Borrego:
    Una quasi-métrica basada en subsunción.
    IV Jornadas Cientificas en Tecnologias de la Informacion. Jornadas Cientificas en Tecnologias de la Informacion. Num. 4. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 260-267
49. José L. Ruiz Reina, Francisco J. Martín, José A. Alonso, María J. Hidalgo:
    Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover.
    Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L'aquila, Italia. 1999. Pag. 289-304
50. Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina:
    Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la inteligencia artificial).
    IV Jornades Sobre L'ensenyament Universitari de la Infomàtica. IV Jornadas Sobre la Enseñanza Universitaria de la Informatica (Jenui'98) (). Andorra. Enginyeria I Arquitectura la Salle. 1998. Pag. 289-296
51. J.J. Arrabal, D. Balbontin, José A. Alonso, F.F. Lara, Francisco J. Martín, M.J. Perez, José L. Ruiz Reina:
    GTI: una herramienta de edición de cursos adaptativos.
    Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634
52. R. Fernández, J.J. Arrabal, José A. Alonso:
    Hacia una enseñanza permanente y automatizada: WWW y evaluación automática con GTI.
    International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1
53. D. Balbontin, M.L. de la Vega, José A. Alonso, J.J. Arrabal:
    Aprende Matemáticas.
    Actas del Primer Encuentro de Informática Educativa: Edie. Primer Encuentro de Informática Educativa (Edie) (). Cees (Madrid). Asociacion para el Desarrollo de la Informatica Educativa. 1994. Pag. 20-25
54. D. Balbontin, José A. Alonso, J.J. Arrabal, F.J. Herrera:
    Especificación formal de bases de datos con un demostrador automático de teoremas.
    Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344
55. D. Balbontin, J.J. Arrabal, José A. Alonso, F.J. Herrera:
    Automated Proofs in Group Theory With OTTER.
    Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331
56. D. Balbontin, José A. Alonso, J.J. Arrabal, F.J. Herrera:
    Razonamiento automático en lógica de primer orden.
    Actas del VIII Congreso de Lenguajes Naturales y Lenguajes Formales. VIII Congreso de Lenguajes Naturales y Lenguajes Formales (). Gerona (España). 1992. Pag. 165-172
57. José A. Alonso, E. Briales, A. Riscos:
    Preuve automatique dans le calcul propositionnel et les logiques trivalentes.
    Computational Topology and Geometry and Computation in Teaching Mathematics. Computational Topology and Geometry and Computation in Teaching of Mathematics. Num. 1. Sevilla. Servicio de Publicaciones de la Universidad de Sevilla. 1990. Pag. 15-24. ISBN: 84-7405-639-X
58. José A. Alonso, E. Briales:
    Lógicas polivalentes y bases de Gröbner.
    V Congreso de Lenguajes Naturales y Lenguajes Formales. Congreso de Lenguajes Naturales y Lenguajes Formales (5). Num. 5. Barcelona, España. Universidad Barcelona. 1989. Pag. 307-315

Tesis dirigidas

1. Director: José A. Alonso y Joaquín Borrego
   Doctorando: Antonio Paredes Moreno:
   Técnicas de depuración e integración de ontologías en el ámbito empresarial,
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2008.
2. Director: Joaquín Borrego,
   Doctorando: Antonia M. Chávez:
   Razonamiento Mereotopológico Automatizado para la Depuración de Ontologías.
   Universidad de Sevilla, Dpto. de Ciencias de la Computación e Inteligencia Artificial, 2005.
3. Director: José A. Alonso,
   Doctorando: María J. Hidalgo:
   Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos,
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2004.
4. Directores: José A. Alonso y José L. Ruiz Reina,
   Doctorando: I. Medina:
   Verificación formal en ACL2 del algoritmo de Buchberger,
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2003.
5. Director: José A. Alonso y Joaquín Borrego
   Doctorando: Miguel A. Gutiérrez:
   Operadores de generalizacion para el aprendizaje clausal,
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2002.
6. Director: José A. Alonso,
   Doctorando: Francisco J. Martín:
   Teoría computacional (en ACL2) sobre cálculos proposicionales,
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2002.
7. Director: José A. Alonso,
   Doctorando: José L. Ruiz Reina:
   Una teoría computacional acerca de la lógica ecuacional (Formalización en ACL2 y demostración automática de sus propiedades),
   Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2000.