Departamento de Ciencias de la Computación e Inteligencia Artificial
Escuela Técnica Superior de Ingeniería Informática
Universidad de Sevilla
Avda. Reina Mercedes, s/n
41012 Sevilla (Spain)
E-mail:
jruiz@us.es,
Phone: (+34) 954557883,
Fax: (+34) 954556599.
Versión en Español
Areas of interest
Research
Publications in books, journals and refereed conferences
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 (USA), 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 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
- A Formally Verified Quadratic Unification Algorithm
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo y F.J. Martín
Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover
and Its Applications (ACL2-2004), 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 and F.J. Martín
in the book Thirty Five Years of Automating Mathematics
edited by Fairouz Kamareddine en the Kluwer Applied Logic series, Kluwer
Academic Publisher.
- A Formal Proof of Dickson's Lemma in ACL2
F.J. Martín, J.A. Alonso, M. J. Hidalgo and J.L. Ruiz Reina
Proceedings of the 10th Int. Conf. on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR 2003), volume 2850 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 and J.L. Ruiz Reina,
Logic Based program synthesis and transformation, LOPSTR 2003, Revised Papers,
volume 2664 of Lecture Notes in Computer Science, Springer Verlag,
2003.
2002
- Formal Proofs About Rewriting Using ACL2
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Annals of Mathematics and Artificial Intelligence 36(3): 239-262 (2002)
Paper
- A Theory About First-order Terms in ACL2
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Paper
- Progress Report: Term Dags Using Stobjs
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Paper
- A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Proceedings of the Third ACL2 workshop, Grenoble 2002
Paper
2001
- Formalizing rewriting in the ACL2 theorem prover
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Artificial Intelligence and Symbolic Computation, AISC 2000, Revised Papers,
volume 1930 of Lecture Notes in Computer Science, Springer Verlag,
2001.
Paper
  ©
Springer-Verlag
- Verifying an applicative ATP using multiset relations
F.J. Martín, J.A. Alonso, M. J. Hidalgo and J.L. Ruiz Reina
Proceedings of EUROCAST 2001, volume 2178 of 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 and F.J. Martín
Proceedings of the Third International Workshop on First-Order Theorem
Proving (FTP 2000), St. Andrews, Scotland. Published as Technical
Report 5-2000, Fachberichte Informatik, Universitat
Koblenz-Landau, 2000.
Paper
- Multiset relations: a tool for proving termination
J.L. Ruiz Reina, J.A. Alonso, M. J. Hidalgo and F.J. Martín
Proceedings of the Second ACL2 workshop, Technical Report TR-00-29,
Computer Science Departament, University of Texas at Austin, 2000.
Paper
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, and M.J. Hidalgo
Proceedings AGP'99, Joint Conference on Declarative Programming,
L'Aquila (Italia), September 1999.
Paper
A book: