Departamento de Ciencias de la Computación e Inteligencia Artificial
Escuela Técnica Superior de Ingeniería Informática
Universidad de Sevilla
Avenida Reina Mercedes, s/n
41012 Sevilla
Correo electrónico:
jruiz@us.es,
Teléfono: 954557883,
Fax: 954556599.
English version
Areas de interés
Investigación
Publicaciones
2011
- "Proof pearl: a formal proof of Higman's lemma in ACL2"
F.J. Martín-Mateos, J.A. Alonso, M. J. Hidalgo and J.L. Ruiz
Reina, Journal of Automated Reasoning, 47(3): pp. 229-250, 2011.
- "Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials"
L. Lambán, F.J. Martín-Mateos, J. Rubio, M. and J.L. Ruiz
Reina, Interactive Theorem Proving 2011 (ITP'11), Lecture Notes in Computer Science 6898 pp.200-215, Springer Verlag, 2011.
2010
- "A verified Common Lisp implementation of Buchberger's algorithm
in ACL2" Inmaculada Medina-Bulo, Francisco Palomo-Lozano and
José Luis Ruiz Reina. Journal of Symbolic Computation 45(1):
pp. 96-123, 2009.
2009
- "ACL2 verification of simplicial degeneracy programs in the Kenzo
system"
F.J. Martín-Mateos, J. Rubio, J.L. Ruiz Reina. Calculemus/MKM 2009,
Lecture Notes in Computer Science 5625 pp.106-121, Springer Verlag, 2009.
2008
- "Constructing Formally Verified Reasoners for the ACC Description Logic"
María-José Hidalgo, José-Antonio Alonso, Francisco-Jesús Martín-Mateos,
José-Luis Ruiz-Reina. Electronic Notes Theoretical Computer Sciences 200(3):
pp. 87-102, 2008.
- "Efficient execution in an automated reasoning environment"
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Stroother Moore,
Sandip Ray, Jose-Luis Ruiz-Reina, Rob Sumners, Daron Vroon and Matt
Wilding., Journal of Functional Programming, Vol. 18, Núm. 01,pp. 15-46 2008.
2007
- "A Formally Verified Prover for the ALC Description
Logic"José-Antonio Alonso, Joaquín Borrego-Díaz, María-José
Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina . TPHOLs
2007, LNCS 4732, pp. 135-150", 2007.
- "Formalizing Simplicial Topology in ACL2" Mirian Andrés,
Laureano Lambán, Julio Rubio, José-Luis Ruiz-Reina: . Seventh International Workshop on the ACL2 Theorem Prover and its Application, Austin, Texas (Estados Unidos), 2007.
2006
- "Formal
Correctness of a Quadratic Unification Algorithm"
José-Luis Ruiz-Reina, Francisco-Jesús Martín-Mateos,
José-Antonio Alonso, María-José Hidalgo. Journal of Automated Reasoning, vol. 37(1-2), pp. 67-92, 2006.
2005
- "Proof Pearl: A Formal Proof of Higman's Lemma in ACL2"
Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina,
José-Antonio Alonso, María-José Hidalgo. TPHOLs 2005, LNCS 3603
pp. 358-372.
2004
- Verification of the Formal Concept Analysis
José-Antonio Alonso, Joaquín Borrego-Díaz,
María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina
Revista de la Real Academia de Ciencias (Serie A Matematicas), 98(1)
pp. 3-16, 2004
- Formal Verification of Molecular Computational Models in ACL2: A
Case Study
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina
Current Topics in Artificial Intelligence
10th Conference of the Spanish Association for Artificial Intelligence, CAEPIA 2003, and 5th Conference on Technology Transfer, TTIA 2003, Revised Selected Papers
volumen 3040 de Lecture Notes in Artificial Intelligence, Springer Verlag, 2004.
- Verified Computer Algebra in ACL2 (Gröbner basis Computation)
I. Medina Bulo, F. Palomo Lozano, J.A. Alonso, J.L Ruiz Reina
Artificial Intelligence and Symbolic Computation
7th International Conference, AISC 2004,
volumen 3249 de Lecture Notes in Artificial Intelligence, Springer Verlag, 2004.
- Formal verification of a generic framework to synthesize SAT-provers
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina
Journal
of Automated Reasoning(32), pp. 287-313, 2004
- Formal reasoning about effcient data structures: a case study in ACL2
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
13th International Symposium LOPSTR 2003, Revised Selected Papers
volumen 3018 de Lecture Notes in Computer Science, Springer Verlag, 2004.
2003
- Termination in ACL2 Using Multiset Relations
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
capítulo
del libro Thirty Five Years of Automating Mathematics
editado por Fairouz Kamareddine en la serie Kluwer Applied Logic, Kluwer
Academic Publisher, Noviembre 2003.
- A Formal Proof of Dickson's Lemma in ACL2
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina
Proceedings of the 10th Int. Conf. on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR 2003), volumen 2850 de Lecture Notes in
Artificial Intelligence, Springer Verlag, 2003.
- Verification in ACL2 of a generic framework to synthetize SAT
provers
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina,
Logic Based program synthesis and transformation, LOPSTR 2002, Revised Papers,
volumen 2664 de Lecture Notes in Computer Science, Springer Verlag,
2003.
2002
- Verificación formal y eficiencia: Un caso de estudio aplicado a
la unificación de términos
J.L. Ruiz Reina, F.J. Martín, J.A. Alonso y M. J. Hidalgo
I Taller
Iberoamericano de Deducción e Inteligencia Artificial, 2002.
Artículo
- Una introducción al análisis formal de conceptos en
PVS
M. J. Hidalgo, F.J. Martín, J.A. Alonso, y J.L. Ruiz Reina
I Taller
Iberoamericano de Deducción e Inteligencia Artificial, 2002.
Artículo
- Desarrollo formal y verificación de sistemas proposicionales
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina
I Taller
Iberoamericano de Deducción e Inteligencia Artificial, 2002.
Artículo
- Formal Proofs About Rewriting Using ACL2
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Annals of Mathematics and Artificial Intelligence 36(3): 239-262 (2002)
Artículo
- A Theory About First-order Terms in ACL2
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Artículo
- Progress Report: Term Dags Using Stobjs
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Artículo
- A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Artículo
2001
- Formalizing rewriting in the ACL2 theorem prover
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Artificial Intelligence and Symbolic Computation, AISC 2000, Revised Papers,
volumen 1930 de Lecture Notes in Computer Science, Springer Verlag,
2001.
Artículo
©
Springer-Verlag
- Formalización del razonamiento ecuacional en una lógica
computacional
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Encuentro de Matemáticos Andaluces, Volumen 2, páginas 41-50.
Artículo
- Verifying an applicative ATP using multiset relations
F.J. Martín, J.A. Alonso, M. J. Hidalgo y J.L. Ruiz Reina
Proceedings of EUROCAST 2001, volumen 2178 de Lecture Notes in Computer
Science, Springer Verlag.
2000
- A mechanical proof of Knuth-Bendix critical pair theorem (using
ACL2)
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Third International Workshop on First-Order Theorem
Proving (FTP 2000), St. Andrews, Escocia. Publicado como Technical
Report 5-2000, páginas 206-216, Fachberichte Informatik, Universitat
Koblenz-Landau, 2000.
Artículo
- Multiset relations: a tool for proving termination
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Second ACL2 workshop, Technical Report TR-00-29,
Computer Science Departament, University of Texas at Austin, 2000.
Artículo
1999
- Mechanical verification of a rule-based unification algorithm in
the Boyer-Moore theorem prover
J.L. Ruiz Reina, F.J. Martín, J.A. Alonso, y M.J. Hidalgo
Proceedings AGP'99, Joint Conference on Declarative Programming,
L'Aquila (Italia), September 1999.
Artículo
1998 y anteriores
- Verificación automática de sistemas de razonamiento
J.L. Ruiz Reina, F.J., Martín, J.A. Alonso, y
M.J. Hidalgo
IV Jornades sobre l'ensenyament univeristari de la
informática (JENUI'98), páginas 297-304, 1998.
Artículo
- Razonamiento automático en sistemas de representación del
conocimiento
F.J., Martín, J.A. Alonso, M.J. Hidalgo y J.L. Ruiz Reina
IV Jornades sobre l'ensenyament univeristari de la
informática (JENUI'98), páginas 289-296, 1998.
- GTI: Una herramienta de edición de cursos adaptativos
J.L. Ruiz Reina, J.A. Alonso, J.J. Arrabal, D. Balbontín,
F.F. Lara, F.J. Martín y M.J. Pérez
Actas del
XIII Congreso Nacional de Ingeniería de Diseño, páginas 627-634, 1997.
- Prueba por consistencia de teoremas inductivos: inducción sin
inducción
J.L. Ruiz Reina y M. E. Gegúndez
Actas del X Congreso de
Lenguajes Naturales y Lenguajes Formales, páginas 597-606, 1994.
Un libro: