Data

NameMartín Mateos, Francisco Jesús
DepartmentCiencias de la Comput. e Int. Artificial
Knowledge areaCiencia de la Computación e Inteligencia Artificial
Professional categoryProfesor Titular de Universidad
E-mailRequest
         

  Statistics

  • Items

    38

  • Visits

    1645

  • Downloads

    1338

  Publications

 

Final Degree Project
Icon

Librería Haskell sobre Model Checking

Martín Mateos, Francisco Jesús; Domínguez Balbás, Pablo (2020-06-01)
In this project we establish the basic theoretical concepts about F inite State M achines and Model Checking so we can ...
Final Degree Project
Icon

Desarrollo de una librería Haskell sobre redes neuronales

Martín Mateos, Francisco Jesús; Ramírez de Arellano Marrero, Antonio (2020-06-01)
Artificial Neural Networks are a computational model whose objective is to simulate the learning system of the human brain, ...
Presentation
Icon

Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms

Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2017-01-01)
We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...
Presentation
Icon

Towards a verifiable topology of data

Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Universidad de La Rioja, Departamento de Matemáticas y Computación, 2016-01-01)
Article
Icon

Modelling algebraic structures and morphisms in ACL2

Heras, Jónathan; Martín Mateos, Francisco Jesús; Pascual, Vico (Springer, 2015-01-01)
In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ...
Article
Icon

Formally Verified Tableau-Based Reasoners for a Description Logic

Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2014-01-01)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
Presentation
Icon

Certified Symbolic Manipulation: Bivariate Simplicial Polynomials

Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (ACM, 2013-01-01)
Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ...
Article
Icon

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

Lambán Pardo, Laureano; Rubio, Julio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Oxford Academic, 2013-01-01)
The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted ...
PhD Thesis
Icon

Formalización en Isar de la metalógica de primer orden

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Serrano Suárez, Fabián Fernando (2012-06-12)
El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. ...
Article
Icon

Formalization of a normalization theorem in simplicial topology

Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2012-01-01)
In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ...
Article
Icon

Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2

Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2011-01-01)
Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ...
Presentation
Icon

Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2011-01-01)
In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ...
Presentation
Icon

Sensorización y control de un proceso de mecanizado utilizando un sistema experto basado en reglas

Serrano Bello, Rafael; González Valencia, Luis Carlos; Martín Mateos, Francisco Jesús (Asociación Española de Dirección e Ingeniería de Proyectos (AEIPRO), 2010-01-01)
Aunque el proceso de fabricación por arranque de viruta ha evolucionado mucho en los últimos años con la incorporación de ...
Chapter of Book
Icon

Topología simplicial en ACL2

Lambán Pardo, Laureano; Romero, Ana; Rubio, Julio; Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Universidad de la Rioja, 2010-01-01)
Presentation
Icon

Expert System to Real Time Control of Machining Processes

Martín Mateos, Francisco Jesús; González Valencia, Luis Carlos; Serrano Bello, Rafael (Springer, 2009-01-01)
Industrial machining processes use automated milling machines. These machines are connected to a control device that ...
Presentation
Icon

ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2009-01-01)
Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It ...
Article
Icon

Constructing Formally Verified Reasoners for the ALC Description Logic

Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Elsevier, 2008-01-01)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...
Presentation
Icon

A Formally Verified Prover for the ALC Description Logic

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2007-01-01)
The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...
Presentation
Icon

KRRT: Knowledge Representation and Reasoning Tutor System

Alonso Jiménez, José Antonio; Aranda, Gonzalo A.; Martín Mateos, Francisco Jesús (Springer, 2007-01-01)
Knowledge Representation & Reasoning (KR&R) is a fundamental topic in Artificial Intelligence. A basic KR language is ...
Article
Icon

Foundational Challenges in Automated Data and Ontology Cleaning in the Semantic Web

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Chávez González, Antonia María; Martín Mateos, Francisco Jesús (IEEE Computer Society, 2006-01-01)
The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the foundational ...
Article
Icon

Formal Correctness of a Quadratic Unification Algorithm

Ruiz Reina, José Luis; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2006-01-01)
We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...
Presentation
Icon

Rete Algorithm Applied to Robotic Soccer

Palomo, M.; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio (Springer, 2005-01-01)
This article is a first approach to the use of Rete algorithm to design a team of robotic soccer playing agents for Robocup ...
Article
Icon

Verification of the Formal Concept Analysis

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Real Academia de Ciencias, 2004-01-01)
This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ...
Article
Icon

Formal verification of a generic framework to synthesize SAT-provers

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2004-01-01)
We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability provers. ...
Presentation
Icon

A Formal Proof of Dickson’s Lemma in ACL2

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003-01-01)
Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...
Presentation
Icon

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

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2003-01-01)
We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...
Presentation
Icon

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

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003-01-01)
Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...
Presentation
Icon

Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Pérez Jiménez, Mario de Jesús; Sancho Caparrini, Fernando (2002-01-01)
In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a ...
Chapter of Book
Icon

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

Graciani Díaz, Carmen; Martín Mateos, Francisco Jesús; Pérez Jiménez, Mario de Jesús (Springer, 2002-01-01)
The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS ...
Presentation
Icon

Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2002-01-01)
We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ...
Article
Icon

Formal proofs about rewriting using ACL2

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2002-01-01)
We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...
Presentation
Icon

A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (University of Texas, 2002-01-01)
In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...
Presentation
Icon

A Theory About First-Order Terms in ACL2

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2002-01-01)
We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...
Presentation
Icon

Progress Report: Term Dags Using Stobjs

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2002-01-01)
We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ...
PhD Thesis
IconIcon

Teoría computacional (en ACL2) sobre cálculos proposicionales

Alonso Jiménez, José Antonio; Martín Mateos, Francisco Jesús (2002-01-01)
En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2.
Presentation
Icon

Verifying an Applicative ATP Using Multiset Relations

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2001-01-01)
We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ...
Presentation
Icon

Formalizing Rewriting in the ACL2 Theorem Prover

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2000-01-01)
We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
Presentation
Icon

Multiset Relations: A Tool for Proving Termination

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2000-01-01)