Diferencia entre revisiones de «Publications»

De WikiGLC
Saltar a: navegación, buscar
(→‎Aportaciones a Congresos)
(→‎Publicaciones en revistas)
 
(No se muestran 109 ediciones intermedias de 6 usuarios)
Línea 1: Línea 1:
 
== Libros ==
 
== Libros ==
−
# {{jalonso}}, {{jborrego}}: ''Agentes Inteligentes: una Aproximación desde la Lógica Computacional''. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5
+
# {{jalonso}}, {{jborrego}}: <br> '''Agentes inteligentes: una aproximación desde la lógica computacional'''. <br> Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5
−
# {{jalonso}}, {{jborrego}}: ''Deducción Automática''. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7
+
# {{jalonso}}, {{jborrego}}: <br> {{j|2002-ded-automatica-1.pdf|Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos)}}. <br> Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7
−
# {{jalonso}}, {{jruiz}}, {{jborrego}}: ''Curso Práctico de Teoría de Conjuntos''. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9
+
# {{jalonso}}, {{jborrego}}, M. Pérez, {{jruiz}}: <br> {{j|2007-LibroTeoriaConjuntos.pdf|Curso práctico de teoría de conjuntos}}. <br> Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9
  
−
== Capítulos en Libros ==
+
== Capítulos en libros ==
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}: ''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
+
# {{garanda}}, {{jborrego}}, {{tchavez}} <br> '''Ontological dimensions of Semantic Mobile Web 2.0. First principles'''.<br> Handbook of Research on Mobility and Computing: Evolving Technologies and Ubiquitous Impacts; pp. 667-688, 2011.
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{fmartin}}, L.C. González y R. Serrano <br> '''Sistema experto para el control en tiempo real de procesos de mecanizado'''.<br> 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.
−
# {{jalonso}}, {{jborrego}}: ''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
+
# {{jalonso}} y F.F. Serrano <br> '''Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar'''.<br> Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{jalonso}}, {{garanda}}, {{jborrego}}<br> '''Sistema certificado de decisión proposicional basado en polinomios'''. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, 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
+
# {{jalonso}} y E.S. Barraza<br> '''Algoritmo para resolver k-SAT basado en cláusulas'''. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}: ''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
+
# {{fmartin}}, {{jruiz}} y L. Lambán<br> '''Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2'''. Workshop on Computational Logics and Artificial Intelligence (CLAI 2009).
−
# {{jalonso}}, {{mjoseh}}, {{jruiz}}, {{fmartin}}: ''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
+
# {{fmartin}}, {{jruiz}}, J. Rubio y L. Lambán <br> '''Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso'''.<br> IX Jornadas sobre Programación y Lenguajes ISBN: 978-84-692-4600-9; pp. 7-14, 2009.
−
# {{jalonso}}, {{jborrego}}: ''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
+
# D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, {{jruiz}}, R. Sumners, D. Vroon and M. Wilding. <br> '''Efficient execution in an automated reasoning environment'''.<br> IX Jornadas sobre Programación y Lenguajes ISBN: 978-84-692-4600-9; pp. 181, 2009.
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}: ''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
+
# {{jborrego}}, {{tchavez}} y {{jalonso}} <br> '''Inconsistency, Logic Databases, and Ontologies'''.<br>  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) [http://www.igi-global.com/reference/details.asp?ID=33444] (Eds.) Viviana E. Ferraggine, Jorge H. Doorn, and Laura C. Rivero, UNICEN.
−
# {{jalonso}}, {{jborrego}}: ''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
+
# {{jborrego}}: <br> '''Inteligencia artificial y la semántica del espacio (virtual).''' Inclusiva-Net: Redes digitales y espacio físico. Media-Lab, Madrid. En Prensa (2008).
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{jalonso}}, {{garanda}} , {{jborrego}}, {{magdalena}} y {{mjoseh}}: <br> '''Extending attribute exploration by means of Boolean derivates'''. <br> 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
−
# J.J. Arrabal, D. Balbontín, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Pérez, {{jruiz}}: ''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
+
#{{garanda}}: <br> '''Tratamiento de la semántica emergente mediante sistemas de agentes basados en conocimiento'''. <br> I Simposio de Doctorado en Web Semántica.(CAEPIA 2007, Salamanca). ISBN:
−
# L. Laita, E. Roanes, {{jalonso}}, 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
+
# {{jborrego}}, {{tchavez}}, {{garanda}}: <br> '''Learning Services Based on Formal Concept Reasoning'''. <br> IADIS International Conference Intelligent Systems and Agents 2007, (IADIS'07). ISBN: 978-972-8924-39-3.(2007).
−
# {{jalonso}}, 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
+
#{{jborrego}}, {{tchavez}}: <br> '''Anomalías en Ontologías Provisionales'''. <br> 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).
−
# J.J. Arrabal, {{jalonso}}, 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
+
# {{jalonso}}, {{jborrego}}, {{tchavez}}: <br> '''Logic Databases and Inconsistency Handling. Encyclopedia of Databases Technologies and Applications'''. <br> Hershey (Pennsylvania), Estados Unidos. Idea Group Reference. Vol. 1. 2006. Pag. 336-340. ISBN: 1-59140-560-2
 +
#{{jalonso}}, {{jborrego}}, {{tchavez}}: <br> '''Fusión Automatizada de Ontologías: Aplicación al Razonamiento Espacial Cualitativo'''. <br> Actas del congreso 50 Años de Inteligencia Artificial. Campus Multidisciplinar en Percepción e Inteligencia, (CMPI'06). ISBN:84-689-9561-4.(2006).
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2004-caepia.pdf|Formal Verification of Molecular Computational Models in ACL2: a Case Study}}. <br> CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. Vol. 2. 2003. Pag. 235-244. ISBN: 84-8373-564-4
 +
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2003-EUROCAST.pdf|Generalizing Logic Programs Via Subsumption}}. <br> 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
 +
# {{jborrego}}, A. Fernández Margarit, M.J. Pérez Jiménez: <br> '''On Sigma-n definability in Arithmetic.''' <br> Philosophical dimensions of Logic and Science, pag 47--56. Kluwer Ac. Press (2003)
 +
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2003-ALS.pdf|Termination in ACL2 Using Multiset Relation}}. <br> Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. Pag. 217-245. ISBN: 1-4020-1656-5
 +
# {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: <br> {{j|2002-IECON.pdf|A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases}}. <br> IECON 2002. Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7475-4
 +
# {{jalonso}}, {{jborrego}}, {{tchavez}}: <br> {{j|2000-EMA-geometria.pdf|Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático}}. <br> 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
 +
# {{jalonso}}, {{mjoseh}}, {{jruiz}}, {{fmartin}}: <br> {{j|2000-EMA-ecuacional.pdf|Formalización del Razonamiento Ecuacional en una Lógica Computacional}}. <br> 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
 +
# {{jalonso}}, {{jborrego}}: <br> {{j|2000-EMA-PLI.pdf|Proximidad entre cláusulas en programación lógica inductiva}}. <br> 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
 +
# {{jalonso}}, {{jborrego}}, {{tchavez}}: <br> {{j|2000-CINTE-EDAT.pdf|Estrategias para la demostración automática de teoremas}}. <br> Libro de Actas Cinte'00. Cadiz. Servicio de Publicaciones de la Universidad de Cádiz. 2000. Pag. 276-283
 +
# {{jalonso}}, {{jborrego}}: <br> '''Interpretación reactiva de sistemas basados en conocimiento.''' <br> Actas del IV Congreso Isko España. Granada. 1999. Pag. 187-193. ISBN: 84-699-0289-X
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|1998-JENUI-rasrc.pdf|Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la inteligencia artificial)}}. <br> 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
 +
# J.J. Arrabal, D. Balbontín, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Pérez, {{jruiz}}: <br> '''GTI: una herramienta de edición de cursos adaptativos.''' <br> Actas del XIII Congreso Nacional de Ingeniería de Proyectos. Sevilla. Antonio F. Martin Navarro. 1997. Pag. 627-634. ISBN: 84-88783-30-2
 +
# L. Laita, E. Roanes, {{jalonso}}, E. Briales: <br> '''Verificación algebraica de SBC Basada en la lógica trievaluada, teoría e implementación.''' <br> 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
 +
# {{jalonso}}, A. Fernández, M.J. Pérez: <br> {{j|1996-ICE-RA.pdf|Razonamiento automático. lógica formal : orígenes, métodos y aplicaciones}}. <br> Sevilla. Kronos S.A. 1995. Pag. 189-211. ISBN: 84-88620-56-X
 +
# J.J. Arrabal, {{jalonso}}, A. Fernández, M.J. Pérez: <br> {{j|1994-LNLF.pdf|Automatización de la aritmética}}. <br> Lenguajes Naturales y Lenguajes Formales X. Barcelona. Ppu: Promociones y Publicaciones Universitarias. 1994. Pag. 167-182. ISBN: 84-477-0396-7
  
−
== Publicaciones en Revistas ==
+
== Publicaciones en revistas ==
−
# David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, {{jruiz}}, Rob Sumners, Daron Vroon and Matthew Wilding. ''Efficient execution in an automated reasoning environment'', Journal of Functional Programming, Vol. 18, Núm. 01, 2008.
+
# {{garanda}}, {{jborrego}} <br> '''Mereotopological Analysis of Formal Concepts in Security Ontologies'''.<br> Advances in Soft Computing 85, pp. 33-40, 2010.
 +
# {{garanda}}, {{jborrego}}, A. Jiménez Mavillard <br> '''Social Ontology Documentation for Knowledge Externalization'''.<br> Communications in Computer and Information Science 108, pp 137--148, 2010.
 +
# {{garanda}}, {{jborrego}} <br> '''Reconciling Knowledge in Social Tagging Web Services'''.<br> LNAI 6077, pp. 383--390, 2010.
 +
# I. Medina, F. Palomo, {{jruiz}}: <br> '''A Verified Common Lisp implementation of Buchberger's algorithm in ACL2'''. <br> Journal of Symbolic Computation. Vol. 45(1). 2010. Pag. 96-123
 +
# {{garanda}}, {{jborrego}}, {{tchavez}} <br> '''Mereotopological Patterns for Ontology Evolution and Debugging'''.<br> IMAGE-A 1(1):151--158 ISSN: 1885-4508, 2010.
 +
# {{garanda}}, {{jborrego}} <br> '''Toward Semantic Mobile Web 2.0 through Multiagent Systems'''.<br> LNAI 5559, pp. 400-409, 2009.
 +
# {{garanda}}, {{jborrego}}, M. Lebrón <br> '''Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations'''.<br> Lecture Notes in Artificial Intelligence, LNAI 5625, pp. 45-58, Springer-Verlag Berlin Heideberg 2009.
 +
# {{fmartin}}, J. Rubio, {{jruiz}} <br> {{ck|2009-calculemus.pdf|ACL2 verification of simplicial degeneracy programs in the Kenzo system}}.<br> Lecture Notes in Artificial Intelligence, LNAI 5625, pp. 106-121, Springer-Verlag Berlin Heideberg 2009.
 +
# {{jborrego}}, {{tchavez}} <br> '''On the Use of Automated Reasoning Systems in Ontology Integration'''.<br>  CEUR Workshop Proceedings 460, pp.  37-48, 2009.
 +
# R. Serrano, L. C. González, {{fmartin}} <br> '''Architecture for the Optimization of a Machining Process in Real Time through Rule-Based Expert System'''.<br> AIP Conference Proceedings, 1181, pp. 652-661, American Institute of Physics 2009.
 +
# {{jborrego}}, {{tchavez}} <br> '''Using Cognitive Entropy to Manage Uncertain Concepts in Formal Ontologies'''.<br>  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.
 +
# D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, {{jruiz}}, R. Sumners, D. Vroon and M. Wilding. <br> [http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457872 '''Efficient execution in an automated reasoning environment'''],<br>  Journal of Functional Programming, Vol. 18, Núm. 01, 2008.
 +
#{{jborrego}}, {{tchavez}}: <br> [http://http://www.springerlink.com/content/kg0r167643x3m076/?p=3668f35d16ba4d379abc1375bcc2e271&pi=38 '''A Formal Foundation for Knowledge Integration of Deficient Information in the Semantic Web'''].<br>  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
 +
# {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: <br> {{j|2007-TPHOLs.pdf|A Formally  Verified Prover for the ALC Description Logic}}.<br>  Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150
 +
#{{jborrego}}, {{tchavez}}: <br> [http://www.springerlink.com/index/0485877208k7k164.pdf '''Visual Ontology Cleaning: Cognitive Principles and Applicability'''].<br>  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
 +
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: <br> {{j|2006-jar.pdf|Formal Correctness of a Quadratic Unification Algorithm}}. <br> Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92
 +
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{fmartin}}: <br> {{j|2006-ieee.pdf|Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning}}. <br> IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52
 +
#{{jborrego}}, {{tchavez}}: <br> [http://www.springerlink.com/content/yq47485788x5823g/?p=453e1fd3170c4228bc98bb892a6e2fd4&pi=32 '''Extension of Ontologies Assisted by Automated Reasoning Systems'''].<br> 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
 +
# {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: <br> {{j|2005-tphols.pdf|Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.}} <br> Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372
 +
#M. Palomo, {{jalonso}}, {{fmartin}}: <br> [http://www.springerlink.com/content/kn51436l17225225/?p=dd8a6ea2f4684b0bb130d28800d41323&pi=74 '''Rete Algorithm Applied to Robotic Soccer.'''] <br> Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576
 +
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2004-LOPSTR.pdf|Formal Reasoning About Efficient Data Structures: a Case Study in ACL2}}. <br> Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2004-JAR.pdf|Formal Verification of a Generic Framework to Synthesize SAT-Provers}}. <br> Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2004-caepia.pdf|Formal Verification of Molecular Computational Models in ACL2: a Case Study}}. <br> Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353
 +
# {{tchavez}}, {{jborrego}}, {{jalonso}}: <br> {{j|2004-DEXA.pdf|Ontology Cleaning By Mereotopological Reasoning}}. <br> Proceedings. 2004. Pag. 132-137
 +
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: <br> {{j|2004-racsam.pdf|Verification of the Formal Concept Analysis}}. <br> RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16
 +
# I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: <br> {{j|2004-aisc.pdf|Verified Computer Algebra in ACL2 (Grobner Bases Computation)}}. <br> Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2003-LPAR.pdf|A Formal Proof of Dickson's Lemma in ACL2}}. <br> Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58
 +
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2003-EUROCAST.pdf|Generalizing Logic Programs Via Subsumption}}. <br> Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126
 +
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{magutier}}, J.D. Navarro: <br> {{j|2003-IEA_AIE.pdf|Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases}}. <br> Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2003-LOPSTR-02.pdf|Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers}}. <br> Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198
 +
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2002-IBERAMIA.pdf|A Quasi-Metric for Machine Learning}}. <br> Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203
 +
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2002-AMAI.pdf|Formal Proofs About Rewriting Using ACL2}}. <br> Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262
 +
# I. Medina, F. Palomo, {{jalonso}}: <br> {{j|2001-TPHOL-poly.pdf|A Certified Polynomial-Based Decision Procedure for Propositional Logic}}. <br> Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312
 +
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2000-AISC.pdf|Formalizing Rewriting in the ACL2 Theorem Prover}}. <br> Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2001-EUROCAST.pdf|Verifying an Applicative ATP Using Multiset Relations}}. <br> Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626
 +
# J. Chazarain, A. Riscos, {{jalonso}}, E. Briales: <br> '''Multivalued-Logic and Gröbner Bases With Applications to Modal Logic.''' <br> Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194
  
−
# {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}:    '''[http://www.cs.us.es/~jalonso/publicaciones/2007-TPHOLs.pdf A Formally  Verified Prover for the ALC Description Logic]'''. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150
+
== Libros de actas ==
−
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: ''Formal Correctness of a Quadratic Unification Algorithm.'' Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92
+
# {{fmartin}}: <br> '''CLAI 2009: Workshop on Computational Logics and Artificial Intelligence.''' <br> Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial. Universidad de Sevilla. 2009
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{fmartin}}: ''Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.'' IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52
+
# {{jalonso}}, {{jruiz}}, {{jborrego}}, M. Ojeda: <br> '''IDEIA 2002: I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial.''' <br> Sevilla. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002
−
# {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: ''Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.'' Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372
 
−
#M. Palomo, {{jalonso}}, {{fmartin}}: ''Rete Algorithm Applied to Robotic Soccer.'' Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576
 
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.'' Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91
 
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Formal Verification of a Generic Framework to Synthesize SAT-Provers.'' Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313
 
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Formal Verification of Molecular Computational Models in ACL2: a Case Study.'' Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353
 
−
# {{tchavez}}, {{jborrego}}, {{jalonso}}: ''Ontology Cleaning By Mereotopological Reasoning.'' Proceedings. 2004. Pag. 132-137
 
−
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: ''Verification of the Formal Concept Analysis.'' RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16
 
−
# I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: ''Verified Computer Algebra in ACL2 (Grobner Bases Computation).'' Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184
 
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''A Formal Proof of Dickson's Lemma in ACL2.'' Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58
 
−
# {{magutier}}, {{jalonso}}, {{jborrego}}: ''Generalizing Programs Via Subsumption.'' Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126
 
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{magutier}}, J.D. Navarro: ''Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases.'' Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798
 
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.'' Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198
 
−
# {{magutier}}, {{jalonso}}, {{jborrego}}: ''A Quasi-Metric for Machine Learning.'' Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203
 
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''Formal Proofs About Rewriting Using ACL2.'' Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262
 
−
# I. Medina, F. Palomo, {{jalonso}}: ''A Certified Polynomial-Based Decision Procedure for Propositional Logic.'' Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312
 
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''Formalizing Rewriting in the Acl2 Theorem Prover.'' Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106
 
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Verifying an Applicative ATP Using Multiset Relations.'' Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626
 
−
# J. Chazarain, A. Riscos, {{jalonso}}, 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 ==
+
== Aportaciones a congresos ==  
−
# {{jalonso}}, {{jruiz}}, {{jborrego}}, M. Ojeda: ''IDEIA 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial.'' Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002
+
# {{fmartin}}, L.C. González y R. Serrano <br> '''Sistema experto para el control en tiempo real de procesos de mecanizado'''.<br> XIII Conferencia de la Asociación Española para la Inteligencia Artificial (CAEPIA-TTIA 2009), Sevilla, 2009.
−
 
+
# E. S. Barraza, {{jalonso}}: <br> '''Algoritmo para resolver k-SAT basado en cláusulas'''.<br> Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
−
== Aportaciones a Congresos ==
+
# {{jalonso}}, {{garanda}}, {{jborrego}}: <br> '''Sistema certificado de decisión proposicional basado en polinomios'''.<br> Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
−
# M. Andres, L. Lamban, J. Rubio, {{jruiz}}: ''Formalizing Simplicial Topology in ACL2''. Seventh International Workshop on the ACL2 Theorem Prover and its Application, Austin, Texas (Estados Unidos), 2007.
+
# {{jalonso}}, F. F. Serrano: <br> '''Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar'''.<br> Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
−
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: ''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
+
# {{fmartin}}, {{jruiz}}, L. Lambán: <br> '''Polinomios simpliciales: una herramienta para la formalización de la Topología Simplicial en ACL2'''.<br> Computational Logics and Artificial Intelligence, (CLAI 2009), Sevilla, 2009.
−
# {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: ''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
+
# {{fmartin}}, {{jruiz}}, J. Rubio, L. Lambán: <br> '''Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso'''.<br> IX Jornadas sobre Programación y Lenguajes, (PROLE 2009), San Sebastián, 2009.
−
# M. Palomo, {{fmartin}}, {{jalonso}}: ''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
+
# D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, {{jruiz}}, R. Sumners, D. Vroon and M. Wilding. <br> '''Efficient execution in an automated reasoning environment'''<br> IX Jornadas sobre Programación y Lenguajes, (PROLE 2009), San Sebastián, 2009.
−
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: ''A Formally Verified Quadratic Unification Algorithm.'' Proceedings of the Fifth International Workshop on the Acl2 Theorem Prover and Its Applications (Acl2-2004). Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32
+
# {{garanda}}, {{jborrego}}, M. Lebrón: <br> '''Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations'''.<br> 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, (CALCULEMUS'09), Ontario (Canadá), 2009.
−
# {{jalonso}}, {{jborrego}}: ''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
+
# {{fmartin}}, J. Rubio, {{jruiz}}: <br> {{ck|2009-calculemus.pdf|ACL2 verification of simplicial degeneracy programs in the Kenzo system}}.<br> 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, (CALCULEMUS'09), Ontario (Canadá), 2009.
−
# {{tchavez}}, {{jalonso}}, {{jborrego}}: ''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
+
# R. Serrano, L.C. González, {{fmartin}}: <br> '''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.
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}: ''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
+
# Antonio Jiménez Mavillard, {{garanda}}, {{jborrego}}: <br> '''Una herramienta para la documentación colaborativa de ontologías'''.<br> Conferencia Internacional de Software Libre 2008 (OSWC 2008).
−
# I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: ''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
+
# {{jborrego}}, {{tchavez}}, {{garanda}}: <br> '''Learning Services Based on Formal Concept Reasoning'''.<br>  IADIS International Conference Intelligent Systems and Agents 2007, (IADIS'07). ISBN: 978-972-8924-39-3.(2007).
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
#{{jborrego}}, {{tchavez}}: <br> '''Anomalías en Ontologías Provisionales'''.<br>  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).
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# M. Andres, L. Lamban, J. Rubio, {{jruiz}}: <br> [http://www.cs.uwyo.edu/~ruben/acl2-07/uploads/Main/007.pdf '''Formalizing Simplicial Topology in ACL2'''].<br>  Seventh International Workshop on the ACL2 Theorem Prover and its Application, Austin, Texas (Estados Unidos), 2007.
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
#{{jalonso}}, {{jborrego}}, {{tchavez}}: <br> '''Fusión Automatizada de Ontologías: Aplicación al Razonamiento Espacial Cualitativo'''.<br>  Actas del congreso 50 Años de Inteligencia Artificial. Campus Multidisciplinar en Percepción e Inteligencia, (CMPI'06). ISBN:84-689-9561-4.(2006).
−
# {{magutier}}, {{jalonso}}, {{jborrego}}: ''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
+
#{{jborrego}}, {{tchavez}}:<br> [http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-173/paper6.pdf '''Controlling Ontology Extension by Uncertain Concepts through Cognitive Entropy'''].<br>  4th International Semantic Web Conference, Workshop on Uncertainty Reasoning for the Semantic Web. Noviembre 2005. Galway, Irlanda.
−
# {{tchavez}}, {{jborrego}}, {{jalonso}}: ''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
+
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: <br> '''A Formally Verified Proof (in PVS) of the Strong Completeness Theorem of Propositional SLD-Resolution.''' <br> 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
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{fmartin}}, {{jruiz}}, {{jalonso}}, {{mjoseh}}: <br> {{j|2005-tphols.pdf|Proof Pearl: a Formal Proof of Higman's Lemma in ACL2}}. <br> 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
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, 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
+
# M. Palomo, {{fmartin}}, {{jalonso}}: <br> [http://www.springerlink.com/content/kn51436l17225225/ '''Rete Algorithm Applied to Robotic Soccer''']. <br> 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
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{magutier}}, J.D. Navarro: ''A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases.'' Proceedings of the Iecon'02. Iecon'02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6
+
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: <br> [http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/ruiz-et-al/qunif-dag.pdf '''A Formally Verified Quadratic Unification Algorithm''']. <br> 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
−
# {{jalonso}}, {{jborrego}}: ''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
+
# {{jalonso}}, {{jborrego}}: <br> {{j|2003-EUROCAST.pdf|Generalizing Logic Programs Via Subsumption}}. <br> 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
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{tchavez}}, {{jalonso}}, {{jborrego}}: <br> {{j|2004-DEXA.pdf|Ontology Cleaning By Mereotopological Reasoning}}. <br> 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
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{jalonso}}, {{jborrego}}, {{tchavez}}: <br> '''Towards a Tool for Ontology Engineering.''' <br> 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
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# I. Medina, F. Palomo, {{jalonso}}, {{jruiz}}: <br> {{j|2004-aisc.pdf|Verified Computer Algebra in ACL2 (Gröbner Basis Computation)}}. <br> 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
−
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{magutier}}: ''Towards a Practical Argumentative Reasoning With Qsd.'' 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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2003-LPAR.pdf|A Formal Proof of Dickson's Lemma in ACL2}}. <br> 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
−
# {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: ''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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2004-LOPSTR.pdf|Formal Reasoning About Efficient Data Structures: a Case Study in ACL2}}. <br> 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
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2004-caepia.pdf|Formal Verification of Molecular Computational Models in ACL2: a Case Study}}. <br> 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
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2003-EUROCAST.pdf|Generalizing Logic Programs Via Subsumption}}. <br> 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
−
# I. Medina, F. Palomo, {{jalonso}}: ''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
+
# {{tchavez}}, {{jborrego}}, {{jalonso}}: <br> {{j|2003-IEA_AIE.pdf|Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases}} <br> (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
−
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: ''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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2002-ACL2-generic.pdf|A Generic Instantiation Tool and a Case Study: a Generic Multiset Theory}}. <br> 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
−
# {{jalonso}}, {{jborrego}}: ''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
+
# {{jalonso}}, {{jborrego}}, {{tchavez}}, J.D. Navarro: <br> {{j|2002-IECON.pdf|A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases}}. <br> 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
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Verifying an Applicative ATP Using Multiset Relations.'' Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626
+
# {{jalonso}}, {{jborrego}}: <br> {{j|2002-IBERAMIA.pdf|A Quasi-Metric for Machine Learning}}. <br> 8th Ibero-American Conference on A.I. Ibero-American Conference on A.I. Num. 8. Sevilla. Springer, Berlín, Alemania. 2002. Pag. 193-203
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2002-ACL2-terms.pdf|A Theory About First-Order Terms in ACL2}}. <br> 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
−
# {{magutier}}, {{jalonso}}, {{jborrego}}: ''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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2002-IDEIA-SAT.pdf|Desarrollo Formal y Verificación de Sistemas Proposicionales}}. <br> 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
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2002-ACL2-dags.pdf|Progress Report: Term Dags Using Stobjs}}.<br>  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
−
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: ''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
+
# {{jalonso}}, {{jborrego}}, {{tchavez}}, {{magutier}}: <br> {{j|2002-IDEIA-spatial.pdf|Towards a Practical Argumentative Reasoning with Qualitative Spatial Database}}. <br> 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
−
# {{magutier}}, {{jalonso}}, {{jborrego}}: ''Una Quasi-Metrica Basada en Subsuncion.'' 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
+
# {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: <br> {{j|2002-IDEIA-AFC.pdf|Una introducción al análisis formal de conceptos en PVS}}. <br> 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
−
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: ''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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2002-IDEIA-unificacion.pdf|Verificación formal y eficiencia: un caso de estudio aplicado a la unificación de términos}}. <br> 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
−
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2003-LOPSTR-02.pdf|Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers}}. <br> 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
−
# J.J. Arrabal, D. Balbontin, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Perez, {{jruiz}}: ''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
+
# I. Medina, F. Palomo, {{jalonso}}: <br> {{j|2001-TPHOL-poly.pdf|A Certified Polynomial-Based Decision Procedure for Propositional Logic}}. <br> 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
−
# R. Fernández, J.J. Arrabal, {{jalonso}}: ''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
+
# {{jalonso}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: <br> {{j|2000-EMA-ecuacional.pdf|Formalización del razonamiento ecuacional en una lógica computacional}}. <br> 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
−
# D. Balbontin, M.L. de la Vega, {{jalonso}}, 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
+
# {{jalonso}}, {{jborrego}}: <br> {{j|2000-EMA-PLI.pdf|Proximidad entre cláusulas en Programación Lógica Inductiva}}. <br> 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
−
# D. Balbontin, {{jalonso}}, 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
+
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|2001-EUROCAST.pdf|Verifying an Applicative ATP Using Multiset Relations}}. <br> Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626
−
# D. Balbontin, J.J. Arrabal, {{jalonso}}, 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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2000-FTP.pdf|A Mechanical Proof of Knuth-Bendix Critical Pair Theorem (Using ACL2)}}. <br> 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
−
# D. Balbontin, {{jalonso}}, 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
+
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2000-ILP.pdf|A Topological Study of the Upward Refinement Operators on ILP}}. <br> 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
−
# {{jalonso}}, 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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2000-AISC.pdf|Formalizing Rewriting in the ACL2 Theorem Prover}}. <br> 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
−
# {{jalonso}}, 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
+
# {{jruiz}}, {{jalonso}}, {{mjoseh}}, {{fmartin}}: <br> {{j|2000-ACL2-multiset.pdf|Multiset Relations: a Tool for Proving Termination}}. <br> Proceedings of the ACL2 Workshop 2000. Second ACL2 Workshop (2). Num. 2. Austin, Texas, EEUU. University of Texas At Austin. 2000. Pag. 82-91
 +
# {{magutier}}, {{jalonso}}, {{jborrego}}: <br> {{j|2000-CINTE-distancia.pdf|Una quasi-métrica basada en subsunción}}. <br> 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
 +
# {{jruiz}}, {{fmartin}}, {{jalonso}}, {{mjoseh}}: <br> {{j|1999-PRODE.pdf|Mechanical Verification of a Rule-Based Unification Algorithm in the Boyer-Moore Theorem Prover}}. <br> Proc. of Joint Conference on Declarative Programming. Joint Conference on Declarative Programming. L'aquila, Italia. 1999. Pag. 289-304
 +
# {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: <br> {{j|1998-JENUI-rasrc.pdf|Razonamiento automático en sistemas de representación del conocimiento (y su relación con la enseñanza de la inteligencia artificial)}}. <br> 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
 +
# J.J. Arrabal, D. Balbontin, {{jalonso}}, F.F. Lara, {{fmartin}}, M.J. Perez, {{jruiz}}: <br> '''GTI: una herramienta de edición de cursos adaptativos.''' <br> Actas del XIII Congreso Nacional de Ingenieria de Proyectos. Journees Détudes Comparatives Franco- Hispano- Italiannes. Num. 1. Burdeos, Francia. 1997. Pag. 627-634
 +
# R. Fernández, J.J. Arrabal, {{jalonso}}: <br> '''Hacia una enseñanza permanente y automatizada: WWW y evaluación automática con GTI.''' <br> International Congress on Historical Information Systems. International Congress on Historical Information Systems (). Vitoria. 1997. Pag. 1-1
 +
# D. Balbontin, M.L. de la Vega, {{jalonso}}, J.J. Arrabal: <br> '''Aprende Matemáticas.''' <br> 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
 +
# D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: <br> '''Especificación formal de bases de datos con un demostrador automático de teoremas.''' <br> Actas del II Congreso Nacional de Programación Declarativa. Congreso Nacional de Programación Declarativa. Num. 2. Sin Editorial. 1993. Pag. 343-344
 +
# D. Balbontin, J.J. Arrabal, {{jalonso}}, F.J. Herrera: <br> {{j|1992-grupos.pdf|Automated Proofs in Group Theory With OTTER}}. <br> Proceedings of the Fith International Symposium on Knowledge Engineering. Fifth International Symposium on Knowledge Engineering (). Sevilla. Rank-Xerox. 1992. Pag. 326-331
 +
# D. Balbontin, {{jalonso}}, J.J. Arrabal, F.J. Herrera: <br> {{j|1992-ralpo.pdf|Razonamiento automático en lógica de primer orden}}. <br> 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
 +
# {{jalonso}}, E. Briales, A. Riscos: <br> '''Preuve automatique dans le calcul propositionnel et les logiques trivalentes.''' <br> 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
 +
# {{jalonso}}, E. Briales: <br> {{j|1990-lpbg.pdf|Lógicas polivalentes y bases de Gröbner}}. <br> 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 ==
 
== Tesis dirigidas ==
−
# Director: {{jalonso}}, Doctorando: {{mjoseh}}: ''Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos'', 2004, Ciencias de la Computacion e Inteligencia Artificial
+
# Director: {{jalonso}} y {{jborrego}} <br> Doctorando: Antonio Paredes Moreno: <br> '''Técnicas de depuración e integración de ontologías en el ámbito empresarial''',<br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2008.
−
# Director: {{jalonso}}, Doctorando: I. Medina: ''Verificación formal en ACL2 del algoritmo de Buchberger'', 2003, Ciencias de la Computacion e Inteligencia Artificial
+
# Director: {{jborrego}}, <br> Doctorando: {{tchavez}}:  <br> '''Razonamiento Mereotopológico Automatizado para la Depuración de Ontologías'''.<br> Universidad de Sevilla, Dpto. de Ciencias de la Computación e Inteligencia Artificial, 2005.
−
# Director: {{jalonso}}, Doctorando: {{magutier}}: ''Operadores de generalizacion para el aprendizaje clausal'', 2002, Ciencias de la Computacion e Inteligencia Artificial
+
# Director: {{jalonso}}, <br> Doctorando: {{mjoseh}}: <br> [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2004-tesis-MJHD.pdf '''Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos'''],<br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2004.
−
# Director: {{jalonso}}, Doctorando: {{fmartin}}: ''Teoría computacional (en ACL2) sobre cálculos proposicionales,'' 2002, Ciencias de la Computacion e Inteligencia Artificial
+
# Directores: {{jalonso}} y {{jruiz}}, <br> Doctorando: I. Medina: <br> [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2003-tesis-IMB.pdf '''Verificación formal en ACL2 del algoritmo de Buchberger'''],<br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2003.
−
# Director: {{jalonso}}, Doctorando: {{jruiz}}: ''Una teoría computacional acerca de la lógica ecuacional (Formalización en ACL2 y demostración automática de sus propiedades)'', 2000, Ciencias de la Computacion e Inteligencia Artificial
+
# Director: {{jalonso}} y {{jborrego}} <br> Doctorando: {{magutier}}: <br> '''Operadores de generalizacion para el aprendizaje clausal''',<br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2002.
 +
# Director: {{jalonso}}, <br> Doctorando: {{fmartin}}: <br> [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2002-tesis-FJMM.pdf '''Teoría computacional (en ACL2) sobre cálculos proposicionales'''], <br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2002.
 +
# Director: {{jalonso}}, <br> Doctorando: {{jruiz}}: <br> [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2001-tesis-JLRR.pdf '''Una teoría computacional acerca de la lógica ecuacional (Formalización en ACL2 y demostración automática de sus propiedades)'''],<br> Universidad de Sevilla, Dpto. de Ciencias de la Computacion e Inteligencia Artificial, 2000.

Revisión actual del 20:02 12 feb 2011

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. 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.
  3. 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).
  4. 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).
  5. 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).
  6. 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).
  7. 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.
  8. 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.
  9. 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.
  10. 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).
  11. 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
  12. 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:
  13. 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).
  14. 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).
  15. 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
  16. 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).
  17. 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
  18. 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
  19. 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)
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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, Antonia M. Chávez
    Mereotopological Patterns for Ontology Evolution and Debugging.
    IMAGE-A 1(1):151--158 ISSN: 1885-4508, 2010.
  6. Gonzalo A. Aranda-Corral, Joaquín Borrego
    Toward Semantic Mobile Web 2.0 through Multiagent Systems.
    LNAI 5559, pp. 400-409, 2009.
  7. 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.
  8. 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.
  9. Joaquín Borrego, Antonia M. Chávez
    On the Use of Automated Reasoning Systems in Ontology Integration.
    CEUR Workshop Proceedings 460, pp. 37-48, 2009.
  10. 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.
  11. 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.
  12. 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.
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. Antonia M. Chávez, Joaquín Borrego, José A. Alonso:
    Ontology Cleaning By Mereotopological Reasoning.
    Proceedings. 2004. Pag. 132-137
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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.
Obtenido de «https://www.glc.us.es/web/index.php?title=Publications&oldid=1024»