José Luis Ruiz Reina

Profesor Titular de Universidad
jruiz@us.es
Área de conocimiento: Ciencia de la Computación e Inteligencia Artificial
Departamento: Ciencias de la Comput. e Int. Artificial
Grupo: LOGICA, COMPUTACION E INGENIERIA DEL CONOCIMIENTO (TIC-137)
Prog. doctorado: Programa de Doctorado en Ingeniería Informática (RD. 99/2011)
Tipo Año Título Fuente
Ponencia2017 Using abstract stobjs in ACL2 to compute matrix normal forms Lecture Notes in Computer Science
Ponencia2016 Towards a verifiable Topology of Data XV Encuentro de Álgebra computacional y aplicaciones: EACA 2016
Artículo2014 Formally Verified Tableau-Based Reasoners for a Description Logic JOURNAL OF AUTOMATED REASONING
Ponencia2014 Proving and computing: Applying automated reasoning to the verification of symbolic computation systems (invited talk) Lecture Notes in Computer Science
Capítulo2014 Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk) Lecture Notes in Computer Science
Artículo2014 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm Logic Journal of the IGPL
Ponencia2013 Certified symbolic manipulation: Bivariate simplicial polynomials Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC
Artículo2012 Formalization of a normalization theorem in simplicial topology ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
Ponencia2011 Applying ACL2 to the formalization of algebraic topology: Simplicial polynomials Lecture Notes in Computer Science
Artículo2011 Proof Pearl: a Formal Proof of Higman's Lemma in ACL2 JOURNAL OF AUTOMATED REASONING
Artículo2010 A verified COMMON LISP implementation of Buchberger's algorithm in ACL2 JOURNAL OF SYMBOLIC COMPUTATION
Capítulo2010 Topología simplicial en ACL2 Contribuciones científicas en honor de Mirian Andrés Gómez
Ponencia2009 ACL2 verification of simplicial degeneracy programs in the kenzo system INTELLIGENT COMPUTER MATHEMATICS, PROCEEDINGS
Ponencia2009 Efficient execution in an automated reasoning environment Programación y lenguajes: IX Jornadas sobre Programación y Lenguajes, PROLE'09, I Taller de Programación Funcional, TPF'09, San Sebastián, España, del 8 al 11 de septiembre de 2009
Ponencia2009 Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso Programación y lenguajes: IX Jornadas sobre Programación y Lenguajes, PROLE'09, I Taller de Programación Funcional, TPF'09, San Sebastián, España, del 8 al 11 de septiembre de 2009
Artículo2008 Efficient execution in an automated reasoning environment JOURNAL OF FUNCTIONAL PROGRAMMING
Ponencia2007 A formally verified prover for the ALC description logic Lecture Notes in Computer Science
Ponencia2007 A formally verified prover for the ALC description logic THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
Artículo2006 Formal correctness of a quadratic unification algorithm JOURNAL OF AUTOMATED REASONING
Ponencia2005 Proof pearl: A formal proof of Higman's Lemma in ACL2 Lecture Notes in Computer Science
Artículo2005 Proof pearl: A formal proof of Higman's lemma in ACL2 THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
Capítulo2005 Topología Simplicial en ACL2 Manual de responsabilidad pública: homenaje a Pedro González Gutiérrez-Barquín
Artículo2004 Formal reasoning about efficient data structures: A case study in ACL2 Lecture Notes in Computer Science
Artículo2004 Formal verification of a generic framework to synthesize SAT-provers JOURNAL OF AUTOMATED REASONING
Ponencia2004 Formal verification of molecular computational models in ACL2: A case study Lecture Notes in Computer Science
Artículo2004 Verified Computer Algebra in ACL2 (Gröbner Bases Computation) Lecture Notes in Computer Science
Artículo2004 Verified computer algebra in ACL2 (Grobner bases computation) ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, PROCEEDINGS
Artículo2003 A formal proof of Dickson's Lemma in ACL2 LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS
Artículo2003 Verification in ACL2 of a generic framework to synthesize SAT-provers LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION
Artículo2002 Formal proofs about rewriting using ACL2 ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
Capítulo2001 Formalización del razonamiento ecuacional en una lógica computacional Actas del Encuentro de Matemáticos Andaluces
Artículo2001 Formalizing rewriting in the ACL2 theorem prover ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION
Ponencia2001 Formalizing rewriting in the ACL2 theorem prover Lecture Notes in Computer Science
Artículo2001 Verifying an applicative ATP using multiset relations COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2001
Ponencia2001 Verifying an applicative ATP using multiset relations Lecture Notes in Computer Science
Ponencia1994 Prueba por consistencia de teoremas inductivos: inducción sin inducción Lenguajes naturales y lenguajes formales : actas del X congreso de lenguajes naturales y lenguajes formales : (Sevilla, 26-30 de septiembre de 1994)
Tesis dirigidas/tutorizadas:1
Fecha lectura Título Rol
18/12/2003 VERIFICACIÓN FORMAL EN ACL2 DEL ALGORITMO DE BUCHBERGER Director/a

Proyectos de Investigación

Fecha de inicio Fecha de fin Rol Denominación Agencia financiadora
01/01/2014 31/12/2017 Investigador/a Lógica Computacional para la Ciencia del Dato (TIN2013-41086-P) Ministerio de Economía y Competitividad (Nacional)
01/01/2010 31/12/2010 Responsable Gestión mecanizada del conocimiento matemático. Aplicaciones en lógica (MTM2009-13842-C02-02) Ministerio de Ciencia e Innovación (Nacional)
13/12/2004 13/12/2007 Investigador/a Sistemas verificados para razonamiento en la Web semántica (TIN2004-03884) Ministerio de Ciencia y Tecnología (Nacional)
28/12/2000 27/12/2003 Investigador/a Desarrollo y verificación formal de sistemas de razonamiento (TIC2000-1368-C03-02) Ministerio de Ciencia y Tecnología (Nacional)