José Luis Ruiz Reina: research and publications

Areas of interest

• Formal methods applied to verification.
• Automated Deduction
• Artificial Intelligence
• Rewriting
• ACL2 user.

Research

• I am a member of the Computational Logic Group of the University of Seville.
• PhD Thesis: Una teoría computacional acerca de la lógica ecuacional, Departamento de Ciencias de la Computación e Inteligencia Artificial, Universidad de Sevilla, September 2001 (in spanish). In postscript format and pdf format. Check also my page about Formalizing equational reasoning in the ACL2 logic (the best option if you do not understand spanish).

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:

• "Curso práctico de teoría de conjuntos" (in spanish), J.A. Alonso, J. Borrego, M.J. Perez, J.L. Ruiz Reina. Ed. La ñ, 1998.