Diferencia entre revisiones de «Publications»
(→Libros) |
|||
| Línea 2: | Línea 2: | ||
{{jalonso}}, Joaquin Borrego Diaz: ''Agentes Inteligentes: una Aproximación desde la Lógica Computacional''. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5 | {{jalonso}}, Joaquin Borrego Diaz: ''Agentes Inteligentes: una Aproximación desde la Lógica Computacional''. Sevilla, España. Editorial Kronos. 2002. 127. ISBN: 84-86273-59-5 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz: ''Deducción Automática''. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7 | |
| − | + | {{jalonso}}, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: ''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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: ''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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, 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}}, Joaquin Borrego Diaz: ''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 | |
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: ''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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: ''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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: | |
Deduccion Automatica 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 | Deduccion Automatica 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}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos: | |
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}}, Joaquin Borrego Diaz: | |
Proximidad Entre Clausulas en Programacion Logica 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 Clausulas en Programacion Logica 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 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: ''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}}, Joaquin Borrego Diaz: ''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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 |
| − | Juan Jose Arrabal Parrilla, Delia Balbontin Noval, | + | Juan Jose Arrabal Parrilla, Delia Balbontin Noval, {{jalonso}}, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis 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 |
| − | Luis Laita, Eugenio Roanes-Lozano, | + | Luis Laita, Eugenio Roanes-Lozano, {{jalonso}}, Emilio Briales Morales: ''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}}, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: ''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 | |
| − | Juan Jose Arrabal Parrilla, | + | Juan Jose Arrabal Parrilla, {{jalonso}}, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: ''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}}, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina: ''A Formally Verified Prover for the ALC Description Logic''. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150 | |
Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: ''Formal Correctness of a Quadratic Unification Algorithm.'' Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92 | Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: ''Formal Correctness of a Quadratic Unification Algorithm.'' Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos: ''Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.'' IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52 | |
Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: ''Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.'' Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372 | Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: ''Proof Pearl: a Formal Proof of Higman S Lemma in ACL2.'' Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372 | ||
| − | Manuel Palomo Duarte, | + | Manuel Palomo Duarte, {{jalonso}}, Francisco Jesus Martin Mateos: ''Rete Algorithm Applied to Robotic Soccer.'' Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576 |
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: ''Formal Reasoning About Efficient Data Structures: a Case Study in ACL2.'' Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91 |
| − | Francisco Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: |
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 Acl2: a Case Study. Lecture Notes in Computer Science. Vol. 3040. 2004. Pag. 344-353 | ||
| − | Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, | + | Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, {{jalonso}}: |
Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137 | Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137 | ||
| − | + | {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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 | Verification of the Formal Concept Analysis. RACSAM. Revista de la Real Academia de Ciencias. Serie a: Matemáticas. Vol. 98. 2004. Pag. 3-16 | ||
| − | Inmaculada Medina Bulo, Francisco Palomo Lozano, | + | Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}, Jose Luis Ruiz Reina: |
Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184 | Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184 | ||
| − | Francisco Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: |
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 Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín: | |
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 | ||
| − | Francisco Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: |
Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198 | Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262 | ||
| − | Inmaculada Medina Bulo, Francisco Palomo Lozano, | + | Inmaculada Medina Bulo, Francisco Palomo Lozano, {{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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | ||
| − | Francisco Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: |
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, Agustin Riscos, | + | J. Chazarain, Agustin Riscos, {{jalonso}}, Emilio Briales Morales: |
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}}, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego: | |
Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. Sevilla, España. Sevilla, España. Departamento de Ciencias de la Computacion e Inteligencia Artificial. Universidad de Sevilla. 2002 | Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. 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}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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 | 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 | ||
| Línea 114: | Línea 114: | ||
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 Acl2 Theorem Prover and Its Applications (Acl2-2004) (5). Num. 5. Austin, Texas, EEUU. Unicersity of Austin. 2004. Pag. 1-32 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz: | |
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 | ||
| − | Antonia Mª Chavez Gonzalez, | + | Antonia Mª Chavez Gonzalez, {{jalonso}}, Joaquin Borrego Diaz: |
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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: | |
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}}, Joaquin Borrego Diaz: | |
Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300 | Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300 | ||
| − | Inmaculada Medina Bulo, Francisco Palomo Lozano, | + | Inmaculada Medina Bulo, Francisco Palomo Lozano, {{jalonso}}, Jose Luis 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 | 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
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 | 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ª Chavez Gonzalez, Joaquin Borrego Diaz, | + | Antonia Mª Chavez Gonzalez, Joaquin Borrego Diaz, {{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 | 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: | |
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 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 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín: | |
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. Proceedings of the Iecon'02. Iecon'02 (). Sevilla, España. IEEE Industrial Electronic Society. 2002. Pag. 1806-1811. ISBN: 0-7803-7474-6 | ||
| − | + | {{jalonso}}, Joaquin Borrego Diaz: | |
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 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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}}, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo: | |
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 | 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}}, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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 | ||
| − | Inmaculada Medina Bulo, Francisco Palomo Lozano, | + | Inmaculada Medina Bulo, Francisco Palomo Lozano, {{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 | 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}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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 | 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}}, Joaquin Borrego Diaz: | |
Proximidad Entre Clausulas en Programacion Logica 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 | Proximidad Entre Clausulas en Programacion Logica 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 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9 | Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9 | ||
| − | Francisco Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | Verifying an Applicative ATP Using Multiset Relations. Eurocast 2001 Conference. Eurocast 2001 Conference. Las Palmas de Gran Canaria. 0. 2001. Pag. 616-626 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
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 | 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 | ||
| − | Miguel Angel Gutierrez Naranjo, | + | Miguel Angel Gutierrez Naranjo, {{jalonso}}, Joaquin Borrego Diaz: |
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 | 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 | ||
| Línea 210: | Línea 210: | ||
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 | 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 Jesus Martin Mateos, | + | Francisco Jesus Martin Mateos, {{jalonso}}, Maria Jose Hidalgo Doblado, Jose Luis 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 | 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 | ||
| − | Jose Luis Ruiz Reina, | + | Jose Luis Ruiz Reina, {{jalonso}}, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: |
Verificación Automática de Sistemas de Razonamiento (Aplicación a 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. 297-304 | Verificación Automática de Sistemas de Razonamiento (Aplicación a 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. 297-304 | ||
| − | Juan Jose Arrabal Parrilla, Delia Balbontin Noval, | + | Juan Jose Arrabal Parrilla, Delia Balbontin Noval, {{jalonso}}, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis 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 | 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 | ||
| Línea 222: | Línea 222: | ||
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 | 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 | ||
| − | Delia Balbontin Noval, Mª Luisa de la Vega Royo, | + | Delia Balbontin Noval, Mª Luisa de la Vega Royo, {{jalonso}}, Juan Jose Arrabal Parrilla: |
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 | 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 | ||
| − | Delia Balbontin Noval, | + | Delia Balbontin Noval, {{jalonso}}, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes: |
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 | 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 | ||
| − | Delia Balbontin Noval, Juan Jose Arrabal Parrilla, | + | Delia Balbontin Noval, Juan Jose Arrabal Parrilla, {{jalonso}}, Francisco Javier Herrera Govantes: |
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 | 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 | ||
| − | Delia Balbontin Noval, | + | Delia Balbontin Noval, {{jalonso}}, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes: |
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 | 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}}, Emilio Briales Morales, Agustin 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 | 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}}, Emilio Briales Morales: | |
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 | 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: | Tesis dirigidas: | ||
| − | Director/a: | + | Director/a: {{jalonso}}, Doctorando: Maria Jose Hidalgo Doblado: |
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 | 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/a: | + | Director/a: {{jalonso}}, Doctorando: Inmaculada Medina Bulo: |
Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial | Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial | ||
| − | Director/a: | + | Director/a: {{jalonso}}, Doctorando: Miguel Angel Gutierrez Naranjo: |
Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial | Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial | ||
| − | Director/a: | + | Director/a: {{jalonso}}, Doctorando: Francisco Jesus Martin Mateos: |
Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial | Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial | ||
| − | Director/a: | + | Director/a: {{jalonso}}, Doctorando: Jose Luis 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 | 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 | ||
Revisión del 20:39 15 abr 2008
Libros
José A. Alonso, Joaquin Borrego Diaz: 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, Joaquin Borrego Diaz: Deducción Automática. Sevilla. Editorial Kronos. 2002. 1004. ISBN: 84-86273-58-7
José A. Alonso, Jose Luis Ruiz Reina, Joaquin Borrego Diaz: Curso Práctico de Teoría de Conjuntos. Sevilla. La Ñ. 1998. 344. ISBN: 84-89524-45-9
Capítulos en Libros
José A. Alonso, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, 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, Joaquin Borrego Diaz: 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: Deduccion Automatica 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, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos: 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, Joaquin Borrego Diaz: Proximidad Entre Clausulas en Programacion Logica 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: 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, Joaquin Borrego Diaz: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Juan Jose Arrabal Parrilla, Delia Balbontin Noval, José A. Alonso, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis 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
Luis Laita, Eugenio Roanes-Lozano, José A. Alonso, Emilio Briales Morales: 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, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: 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
Juan Jose Arrabal Parrilla, José A. Alonso, Alejandro Fernandez Margarit, Mario Jesus Perez Jimenez: 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, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina: A Formally Verified Prover for the ALC Description Logic. Lecture Notes in Computer Science. Vol. 4732. 2007. Pag. 135-150
Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: Formal Correctness of a Quadratic Unification Algorithm. Journal of Automated Reasoning. Vol. 37. Núm. 1-2. 2006. Pag. 67-92
José A. Alonso, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Francisco Jesus Martin Mateos: Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning. IEEE Intelligent Systems. Vol. 21. Núm. 1. 2006. Pag. 42-52
Francisco Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: Proof Pearl: a Formal Proof of Higman S Lemma in ACL2. Lecture Notes in Computer Science. Vol. 3603. 2005. Pag. 358-372
Manuel Palomo Duarte, José A. Alonso, Francisco Jesus Martin Mateos: Rete Algorithm Applied to Robotic Soccer. Lecture Notes in Computer Science. Vol. 3643. 2005. Pag. 571-576
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: Formal Reasoning About Efficient Data Structures: a Case Study in ACL2. Lecture Notes in Computer Science. Vol. 3018. 2004. Pag. 75-91
Francisco Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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ª Chavez Gonzalez, Joaquin Borrego Diaz, José A. Alonso: Ontology Cleaning By Mereotopological Reasoning. Proceedings. 2004. Pag. 132-137
José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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
Inmaculada Medina Bulo, Francisco Palomo Lozano, José A. Alonso, Jose Luis Ruiz Reina: Verified Computer Algebra in Acl2 (Grobner Bases Computation). Lecture Notes in Computer Science. Vol. 3249. 2004. Pag. 171-184
Francisco Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: A Formal Proof of Dickson's Lemma in Acl2. Lecture Notes in Computer Science. Vol. 2850. 2003. Pag. 49-58
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: Generalizing Programs Via Subsumption. Lecture Notes in Computer Science. Vol. 2809. 2003. Pag. 115-126
José A. Alonso, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín: Towards a Practical Argumentative Reasoning With Qualitative Spatial Databases. Lecture Notes in Computer Science. Vol. 2718. 2003. Pag. 789-798
Francisco Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: Verification in Acl2 of a Generic Framework to Synthesize SAT-Provers. Lecture Notes in Computer Science. Vol. 2664. 2003. Pag. 182-198
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: A Quasi-Metric for Machine Learning. Lecture Notes in Computer Science. Vol. 2527. 2002. Pag. 193-203
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: Formal Proofs About Rewriting Using Acl2. Annals of Mathematics and Artificial Intelligence . Vol. 36. Núm. 3. 2002. Pag. 239-262
Inmaculada Medina Bulo, Francisco Palomo Lozano, José A. Alonso: A Certified Polynomial-Based Decision Procedure for Propositional Logic. Lecture Notes in Computer Science. Núm. 2152. 2001. Pag. 297-312
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: Formalizing Rewriting in the Acl2 Theorem Prover. Lecture Notes in Computer Science. Vol. 1930. 2001. Pag. 92-106
Francisco Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis Ruiz Reina: Verifying an Applicative ATP Using Multiset Relations. Lecture Notes in Computer Science. Vol. 2178. 2001. Pag. 612-626
J. Chazarain, Agustin Riscos, José A. Alonso, Emilio Briales Morales: 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, Jose Luis Ruiz Reina, Joaquin Borrego Diaz, Manuel Ojeda Aciego: Ideia 2002: I Taller Iberoamericano Sobre Deducción Automática e Inteligencia Artificial. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. Num. 1. 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, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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 Jesus Martin Mateos, Jose Luis Ruiz Reina, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: 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
Manuel Palomo Duarte, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez: 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
Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: 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, Joaquin Borrego Diaz: 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ª Chavez Gonzalez, José A. Alonso, Joaquin Borrego Diaz: 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez: 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
José A. Alonso, Joaquin Borrego Diaz: Towards a Tool for Ontology Engineering. Advances in Roboticas. Vol 4. Wac 2004. Wac (World Automation Congress) (). Sevilla, España. Tsi Press. 2004. Pag. 1-300
Inmaculada Medina Bulo, Francisco Palomo Lozano, José A. Alonso, Jose Luis 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: 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ª Chavez Gonzalez, Joaquin Borrego Diaz, 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Jorge D. Navarro Marín: 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo, Jorge D. Navarro Marín: 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, Joaquin Borrego Diaz: 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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, Joaquin Borrego Diaz, Antonia Mª Chavez Gonzalez, Miguel Angel Gutierrez Naranjo: 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, Joaquin Borrego Diaz, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Inmaculada Medina Bulo, Francisco Palomo Lozano, 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, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos, Jose Luis 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, Joaquin Borrego Diaz: Proximidad Entre Clausulas en Programacion Logica 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
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: Proximidad Entre Cláusulas en Programación Lógica Inductiva. Actas del Encuentro de Matemáticos Andaluces: Comunicaciones. Encuentro de Matemáticos Andaluces (). Sevilla, España. Servicio de Publicaciones de la Universidad de Sevilla. 2001. Pag. 33-40. ISBN: 84-472-0290-9
Francisco Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: 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
Miguel Angel Gutierrez Naranjo, José A. Alonso, Joaquin Borrego Diaz: 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
Jose Luis Ruiz Reina, Francisco Jesus Martin Mateos, Jose Antonio Alonso Jimenez, Maria Jose Hidalgo Doblado: 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 Jesus Martin Mateos, José A. Alonso, Maria Jose Hidalgo Doblado, Jose Luis 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
Jose Luis Ruiz Reina, José A. Alonso, Maria Jose Hidalgo Doblado, Francisco Jesus Martin Mateos: Verificación Automática de Sistemas de Razonamiento (Aplicación a 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. 297-304
Juan Jose Arrabal Parrilla, Delia Balbontin Noval, José A. Alonso, Francisco Felix Lara Martin, Francisco Jesus Martin Mateos, Mario Jesus Perez Jimenez, Jose Luis 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
Rodrigo Fernandez Carrion, Juan Jose Arrabal Parrilla, Jose Antonio Alonso Jimenez: 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
Delia Balbontin Noval, Mª Luisa de la Vega Royo, José A. Alonso, Juan Jose Arrabal Parrilla: 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
Delia Balbontin Noval, José A. Alonso, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes: 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
Delia Balbontin Noval, Juan Jose Arrabal Parrilla, José A. Alonso, Francisco Javier Herrera Govantes: 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
Delia Balbontin Noval, José A. Alonso, Juan Jose Arrabal Parrilla, Francisco Javier Herrera Govantes: 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, Emilio Briales Morales, Agustin 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, Emilio Briales Morales: 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/a: José A. Alonso, Doctorando: Maria Jose Hidalgo Doblado: 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/a: José A. Alonso, Doctorando: Inmaculada Medina Bulo: Verificación Formal en Acl2 del Algoritmo de Buchberger, 2003, Ciencias de la Computacion e Inteligencia Artificial
Director/a: José A. Alonso, Doctorando: Miguel Angel Gutierrez Naranjo: Operadores de Generalizacion para el Aprendizaje Clausal, 2002, Ciencias de la Computacion e Inteligencia Artificial
Director/a: José A. Alonso, Doctorando: Francisco Jesus Martin Mateos: Teoría Computacional (en Acl2) Sobre Cálculos Proposicionales, 2001, Ciencias de la Computacion e Inteligencia Artificial
Director/a: José A. Alonso, Doctorando: Jose Luis 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
