Diferencia entre revisiones de «Publications»
| Línea 1: | Línea 1: | ||
== Libros == | == Libros == | ||
| − | {{jalonso}}, | + | {{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}}, | + | {{jalonso}}, {{jborrego}}: ''Deducción Automática''. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7 |
| − | {{jalonso}}, | + | {{jalonso}}, {{jruiz}}, {{jborrego}}: ''Curso Práctico de Teoría de Conjuntos''. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9 |
== Capítulos en Libros == | == Capítulos en Libros == | ||
| − | {{jalonso}}, | + | {{jalonso}}, {{jborrego}}, {{tchavez}}: ''Logic Databases and Inconsistgency 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 |
| − | + | {{fmartin}}, {{jalonso}}, {{mjoseh}}, Jose Luis 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 | |
| − | {{jalonso}}, | + | {{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 |
| − | + | {{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}}, | + | {{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}}, | + | {{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 |
| − | |||
| − | {{jalonso}}, | + | {{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 |
| − | 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 | ||
| − | {{jalonso}}, | + | {{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 |
| − | Proximidad Entre | ||
| − | {{jalonso}}, | + | {{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 |
| − | {{jalonso}}, | + | {{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 |
| − | + | {{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 | |
| − | + | 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 | |
| − | + | 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 | |
| − | {{jalonso}}, | + | {{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 |
| − | + | 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 | |
| − | == Publicaciones en Revistas == | + | ================= Publicaciones en Revistas ================= |
| − | {{jalonso}}, | + | {{jalonso}}, {{jborrego}}, {{mjoseh}}, {{fmartin}}, {{jruiz}}: ''A Formally Verified Prover for the ALC Description Logic''. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150 |
| − | + | {{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 | |
| − | {{jalonso}}, | + | {{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 |
| − | + | {{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 | |
| − | Formal Verification of Molecular Computational Models in | ||
| − | + | {{tchavez}}, {{jborrego}}, {{jalonso}}: ''Ontology Cleaning By Mereotopological Reasoning.'' Proceedings. 2004. Pag. 132-137 | |
| − | Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137 | ||
| − | {{jalonso}}, | + | {{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 |
| − | 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 | |
| − | Verified Computer Algebra in | ||
| − | + | {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''A Formal Proof of Dickson's Lemma in ACL2.'' Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58 | |
| − | A Formal Proof of Dickson's Lemma in | ||
| − | + | M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: ''Generalizing Programs Via Subsumption.'' Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126 | |
| − | Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126 | ||
| − | {{jalonso}}, | + | {{jalonso}}, {{jborrego}}, {{tchavez}}, M.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 |
| − | 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 | |
| − | Verification in | ||
| − | + | M.A. Gutiérrez, {{jalonso}}, {{jborrego}}: ''A Quasi-Metric for Machine Learning.'' Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203 | |
| − | 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 | |
| − | Formal Proofs About Rewriting Using | ||
| − | + | 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 | |
| − | 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 | |
| − | 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 | |
| − | Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626 | ||
| − | J. Chazarain, | + | 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 |
| − | Multivalued-Logic and Gröbner Bases With Applications to Modal Logic. Journal of Symbolic Computation . Vol. 11. 1991. Pag. 181-194 | ||
| − | Libros de Actas | + | == Libros de Actas == |
| − | {{jalonso}}, | + | {{jalonso}}, {{jruiz}}, {{jborrego}}, M. Ojeda: ''IDIA 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 |
| − | |||
| − | Aportaciones a Congresos | + | == Aportaciones a Congresos == |
| − | {{jalonso}}, | + | {{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 |
| − | A Formally Verified Proof (in PVS) of the Strong Completeness Theorem Of Propositional | ||
| − | + | {{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 | |
| − | Proof Pearl: a Formal Proof of Higman's Lemma in | ||
| − | + | 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 | |
| − | 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 | ||
| − | + | {{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 | |
| − | 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 | ||
| − | {{jalonso}}, | + | {{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 |
| − | 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 | ||
| − | + | {{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 | |
| − | 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 | ||
| − | {{jalonso}}, | + | {{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 |
| − | 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 | ||
| − | {{jalonso}}, | + | 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 |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | Formal | ||
| − | + | M.A. Gutiérrez, {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | A | ||
| − | {{jalonso}}, | + | {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez, 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 |
| − | A Methodology for the Computer-Aided Cleaning of Complex Knowledge Databases. | ||
| − | {{jalonso}}, | + | {{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 |
| − | A | ||
| − | {{jalonso}}, | + | {{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 |
| − | A | ||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{jalonso}}, {{jborrego}}, {{tchavez}}, M.A. Gutiérrez: ''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 | |
| − | |||
| − | {{jalonso}}, | + | {{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 |
| − | |||
| − | {{jalonso}}, | + | {{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}}: ''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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | {{jalonso}}, | + | {{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}}, | + | {{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 |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | M.A. Gutiérrez, {{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 | |
| − | |||
| − | + | {{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}}: ''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 | |
| − | |||
| − | + | M.A. Gutiérrez, {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | 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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | {{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 | |
| − | |||
| − | + | == 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 | |
| − | {{jalonso}}, | + | Director: {{jalonso}}, Doctorando: I. Medina: ''Verificación formal en ACL2 del algoritmo de Buchberger'', 2003, Ciencias de la Computacion e Inteligencia Artificial |
| − | |||
| − | {{jalonso}}, | + | Director: {{jalonso}}, Doctorando: M.A. Gutiérrez: ''Operadores de generalizacion para el aprendizaje clausal'', 2002, Ciencias de la Computacion e Inteligencia Artificial |
| − | |||
| − | + | Director: {{jalonso}}, Doctorando: {{fmartin}}: ''Teoría computacional (en ACL2) sobre cálculos proposicionales,'' 2002, Ciencias de la Computacion e Inteligencia Artificial | |
| − | Director | ||
| − | Teoría | ||
| − | Director | + | 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 |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | Una | ||
Revisión del 21:18 15 abr 2008
Sumario
Libros
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
José A. Alonso, Joaquín Borrego: Deducción Automática. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7
José A. Alonso, José L. Ruiz Reina, Joaquín Borrego: Curso Práctico de Teoría de Conjuntos. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9
Capítulos en Libros
José A. Alonso, Joaquín Borrego, Antonia M. Chávez: Logic Databases and Inconsistgency 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
Francisco J. Martín, José A. Alonso, María J. Hidalgo, Jose Luis 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
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
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
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
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
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
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
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
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
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
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
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
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
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 ===========
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
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
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
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
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
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
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
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
Antonia M. Chávez, Joaquín Borrego, José A. Alonso: Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137
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
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
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
M.A. Gutiérrez, José A. Alonso, Joaquín Borrego: Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126
José A. Alonso, Joaquín Borrego, Antonia M. Chávez, M.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
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
M.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
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
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
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
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
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
José A. Alonso, José L. Ruiz Reina, Joaquín Borrego, M. Ojeda: IDIA 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
Aportaciones a Congresos
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
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
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
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). 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
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
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
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
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
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
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
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
M.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
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
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
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
José A. Alonso, Joaquín Borrego, Antonia M. Chávez, M.A. Gutiérrez, 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
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
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
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
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
José A. Alonso, Joaquín Borrego, Antonia M. Chávez, M.A. Gutiérrez: 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
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
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
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
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
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
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
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
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
M.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
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
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
M.A. Gutiérrez, José A. Alonso, Joaquín Borrego: 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
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
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
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
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
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
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
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
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
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
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
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, 2004, Ciencias de la Computacion e Inteligencia Artificial
Director: José A. Alonso, Doctorando: I. Medina: Verificación formal en ACL2 del algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial
Director: José A. Alonso, Doctorando: M.A. Gutiérrez: Operadores de generalizacion para el aprendizaje clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial
Director: José A. Alonso, Doctorando: Francisco J. Martín: Teoría computacional (en ACL2) sobre cálculos proposicionales, 2002, Ciencias de la Computacion e Inteligencia Artificial
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), 2000, Ciencias de la Computacion e Inteligencia Artificial
