José-Antonio Alonso

Antonio Hernando

Math. Comput. Simul., 2014

2011

A logic approach to decision taking in a railway interlocking system using Maple.

[BibT_eX]

[DOI]

Eugenio Roanes-Lozano

Antonio Hernando

Luis M. Laita

Math. Comput. Simul., 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

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]

J. Autom. Reason., 2006

Consistency in the Analytic Hierarchy Process: a New Approach.

[BibT_eX]

[DOI]

M. Teresa Lamata

Int. J. Uncertain. Fuzziness Knowl. Based Syst., 2006

2005

A Statistical Criterion of Consistency in the Analytic Hierarchy Process.

[BibT_eX]

[DOI]

María Teresa Lamata

Proceedings of the Modeling Decisions for Artificial Intelligence, 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 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

A computer algebra approach to verification and deduction in many-valued knowledge systems.

[BibT_eX]

[DOI]

Luis M. Laita

Eugenio Roanes-Lozano

Luis de Ledesma

Soft Comput., 1999

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

[BibT_eX]