default search action

combined dblp search
author search
venue search
publication search

ask others

José-Luis Ruiz-Reina

> Home > Persons

Person information

affiliation: University of Seville, Spain

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

2010 – 2019

see FAQ

What is the meaning of the colors in the publication lists?

2017
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/LambanMRR17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LambanMRR17
Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. ITP 2017: 354-370
2014
[j9]
- view
  authority control:
- export record
  dblp key:
  - journals/igpl/LambanRMR14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/igpl/LambanRMR14
Laureano Lambán, Julio Rubio, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Log. J. IGPL 22(1): 39-65 (2014)
[j8]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Hidalgo-DobladoABMR14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Hidalgo-DobladoABMR14
María-José Hidalgo-Doblado, José A. Alonso-Jiménez, Joaquín Borrego-Díaz, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
Formally Verified Tableau-Based Reasoners for a Description Logic. J. Autom. Reason. 52(3): 331-360 (2014)
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/aisc/Ruiz-Reina14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aisc/Ruiz-Reina14
José-Luis Ruiz-Reina:
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk). AISC 2014: 1-6
2013
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/issac/LambanMRR13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/issac/LambanMRR13
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Certified symbolic manipulation: bivariate simplicial polynomials. ISSAC 2013: 243-250
2012
[j7]
- view
  authority control:
- export record
  dblp key:
  - journals/amai/LambanMRR12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/amai/LambanMRR12
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Formalization of a normalization theorem in simplicial topology. Ann. Math. Artif. Intell. 64(1): 1-37 (2012)
2011
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Martin-MateosRAH11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Martin-MateosRAH11
Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo:
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. J. Autom. Reason. 47(3): 229-250 (2011)
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/LambanMRR11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LambanMRR11
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. ITP 2011: 200-215
2010
[j5]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jsc/Medina-BuloPR10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jsc/Medina-BuloPR10
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José-Luis Ruiz-Reina:
A verified Common Lisp implementation of Buchberger's algorithm in ACL2. J. Symb. Comput. 45(1): 96-123 (2010)

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/mkm/Martin-MateosRR09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/mkm/Martin-MateosRR09
Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. Calculemus/MKM 2009: 106-121
2008
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/GreveKMMRRSVW08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/GreveKMMRRSVW08
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding:
Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1): 15-46 (2008)
2007
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/AlonsoBHMR07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/AlonsoBHMR07
José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
A Formally Verified Prover for the ALC Description Logic. TPHOLs 2007: 135-150
[c10]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/HidalgoAMR08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/HidalgoAMR08
María-José Hidalgo, José-Antonio Alonso, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
Constructing Formally Verified Reasoners for the ACL Description Logic. WWV 2007: 87-102
2006
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Ruiz-ReinaMAH06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Ruiz-ReinaMAH06
José-Luis Ruiz-Reina, Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo:
Formal Correctness of a Quadratic Unification Algorithm. J. Autom. Reason. 37(1-2): 67-92 (2006)
2005
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Martin-MateosRAH05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Martin-MateosRAH05
Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo:
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. TPHOLs 2005: 358-372
2004
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Martin-MateosAHR04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Martin-MateosAHR04
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina:
Formal Verification of a Generic Framework to Synthetize SAT-Provers. J. Autom. Reason. 32(4): 287-313 (2004)
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/aisc/Medina-BuloPAR04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aisc/Medina-BuloPAR04
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez, José-Luis Ruiz-Reina:
Verified Computer Algebra in Acl2. Gröbner Bases Computation. AISC 2004: 171-184
2003
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/caepia/Martin-MateosAHR03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/caepia/Martin-MateosAHR03
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina:
Formal Verification of Molecular Computational Models in ACL2: A Case Study. CAEPIA 2003: 344-353
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/lopstr/Ruiz-ReinaJHM03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lopstr/Ruiz-ReinaJHM03
José-Luis Ruiz-Reina, José Antonio Alonso Jimenez, María-José Hidalgo, Francisco-Jesús Martín-Mateos:
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. LOPSTR 2003: 75-91
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/Martin-MateosAHR03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Martin-MateosAHR03
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina:
A Formal Proof of Dickson's Lemma in ACL2. LPAR 2003: 49-58
2002
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/amai/Ruiz-ReinaAHM02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/amai/Ruiz-ReinaAHM02
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos:
Formal Proofs About Rewriting Using ACL2. Ann. Math. Artif. Intell. 36(3): 239-262 (2002)
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/lopstr/Martin-MateosAHR02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lopstr/Martin-MateosAHR02
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina:
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers. LOPSTR 2002: 182-198
2001
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/eurocast/Martin-MateosAHR01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/eurocast/Martin-MateosAHR01
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina:
Verifying an Applicative ATP Using Multiset Relations. EUROCAST 2001: 612-626
2000
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/aisc/Ruiz-ReinaAHM00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aisc/Ruiz-ReinaAHM00
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos:
Formalizing Rewriting in the ACL2 Theorem Prover. AISC 2000: 92-106

1990 – 1999

see FAQ

What is the meaning of the colors in the publication lists?

1999
[c1]
- no documents available
  - details & citations
- export record
  dblp key:
  - conf/agp/Ruiz-ReinaAHM99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/agp/Ruiz-ReinaAHM99
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos:
Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. APPIA-GULP-PRODE 1999: 289-304

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.