María-José Hidalgo

J. Autom. Reason., 2014

2011

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

[BibT_eX]

[DOI]

J. Autom. Reason., 2011

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

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]