Francisco-Jesús Martín-Mateos

Francisco J. Martín-Mateos

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

2015

Modelling algebraic structures and morphisms in ACL2.

[BibT_eX]

[DOI]

Jónathan Heras

María-José Hidalgo-Doblado

Vico Pascual

Appl. Algebra Eng. Commun. Comput., 2015

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

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

2009

ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

Expert System to Real Time Control of Machining Processes.

[BibT_eX]

[DOI]

Luis Carlos González Valencia

Rafael Serrano Bello

Proceedings of the Current Topics in Artificial Intelligence, 2009

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

KRRT: Knowledge Representation and Reasoning Tutor System.

[BibT_eX]

[DOI]

Francisco J. Martín-Mateos

Gonzalo A. Aranda-Corral

Proceedings of the Computer Aided Systems Theory, 2007

2006

Formal Correctness of a Quadratic Unification Algorithm.

[BibT_eX]

[DOI]

Antonia M. Chávez-González

J. Autom. Reason., 2006

Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.

[BibT_eX]

[DOI]

José A. Alonso-Jiménez

Joaquín Borrego-Díaz

IEEE Intell. Syst., 2006

2005

Rete Algorithm Applied to Robotic Soccer.

[BibT_eX]

[DOI]

Manuel Palomo-Duarte

Proceedings of the Computer Aided Systems Theory, 2005

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

Specification of Adleman's Restricted Model Using an Automated Reasoning System: Verification of Lipton's Experiment.

[BibT_eX]

[DOI]

Carmen Graciani Díaz

Mario J. Pérez-Jiménez

Proceedings of the Unconventional Models of Computation, Third International Conference, 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]