José-Luis Ruiz-Reina

Francisco J. Martín-Mateos

María-José Hidalgo-Doblado

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2014

Formally Verified Tableau-Based Reasoners for a Description Logic.

[BibT_eX]

[DOI]

José A. Alonso-Jiménez

Joaquín Borrego-Díaz

J. Autom. Reason., 2014

Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm.

[BibT_eX]

[DOI]

Log. J. IGPL, 2014

Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2014

2013

Certified symbolic manipulation: bivariate simplicial polynomials.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 2013

2012

Formalization of a normalization theorem in simplicial topology.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2012

2011

Proof Pearl: a Formal Proof of Higman's Lemma in ACL2.

[BibT_eX]

[DOI]

J. Autom. Reason., 2011

Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

A verified Common Lisp implementation of Buchberger's algorithm in ACL2.

[BibT_eX]

[DOI]

Inmaculada Medina-Bulo

Francisco Palomo-Lozano

J. Symb. Comput., 2010

2009

ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Efficient execution in an automated reasoning environment.

[BibT_eX]

[DOI]

J. Funct. Program., 2008

2007

Constructing Formally Verified Reasoners for the ACL Description Logic.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, 2007

A Formally Verified Prover for the <i>ALC</i> Description Logic.

[BibT_eX]

[DOI]

Joaquín Borrego-Díaz

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

Formal Correctness of a Quadratic Unification Algorithm.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

2004

Formal Verification of a Generic Framework to Synthetize SAT-Provers.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

Verified Computer Algebra in Acl2. Gröbner Bases Computation.

[BibT_eX]

[DOI]

Inmaculada Medina-Bulo

Francisco Palomo-Lozano

José A. Alonso-Jiménez

Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

2003

A Formal Proof of Dickson's Lemma in ACL2.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

Formal Reasoning about Efficient Data Structures: A Case Study in ACL2.

[BibT_eX]

[DOI]

José Antonio Alonso Jimenez

Proceedings of the Logic Based Program Synthesis and Transformation, 2003

Formal Verification of Molecular Computational Models in ACL2: A Case Study.

[BibT_eX]

[DOI]

Proceedings of the Current Topics in Artificial Intelligence, 2003

2002

Formal Proofs About Rewriting Using ACL2.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2002

Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Tranformation, 2002

2001

Verifying an Applicative ATP Using Multiset Relations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Systems Theory, 2001

2000

Formalizing Rewriting in the ACL2 Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2000

1999

Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover.

[BibT_eX]