Perfil del autor: Martín Mateos, Francisco Jesús
Datos institucionales
| Nombre | Martín Mateos, Francisco Jesús |
| Departamento | Ciencias de la Computación e Inteligencia Artificial |
| Área de conocimiento | Ciencia de la Computación e Inteligencia Artificial |
| Categoría profesional | Profesor Titular de Universidad |
| Correo electrónico | Solicitar |
 |
|
Estadísticas
-
Nº publicaciones
43
-
Nº visitas
3519
-
Nº descargas
4209
| Publicaciones |
|---|
Trabajo Fin de Grado
 Librería sobre grafos en Haskell : el problema del camino más corto
(2023)
The shortest path problem is an important problem in graph theory, consisting in finding paths between two nodes in weighted ... |
Trabajo Fin de Grado
Librería sobre esteganografía en Haskell
(2023)
Steganography is the art of hiding the fact that comunication is taking place. In this project we present an introduction ... |
| Trabajo Fin de Grado |
Trabajo Fin de Grado
Desarrollo de una librería Haskell sobre árboles de decisión
(2021)
A Decision Tree is a supervised learning technique used for prediction tasks, which stands out for being able to produce ... |
Trabajo Fin de Grado
Desarrollo de una librería Haskell sobre códigos QR
(2021)
QR codes are the most common way of storing and exchanging information. In this project they will be studied in order to create a Haskell package with necessary functions and data types to implement them. |
Trabajo Fin de Grado
Desarrollo de una librería Haskell sobre redes neuronales
(2020)
Artificial Neural Networks are a computational model whose objective is to simulate the learning system of the human brain, ... |
Trabajo Fin de Grado
Librería Haskell sobre Model Checking
(2020)
In this project we establish the basic theoretical concepts about F inite State M achines and Model Checking so we can ... |
Ponencia
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
(Springer, 2017)
We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ... |
Ponencia
Towards a verifiable topology of data
(Universidad de La Rioja, Departamento de Matemáticas y Computación, 2016)
|
Artículo
Modelling algebraic structures and morphisms in ACL2
(Springer, 2015)
In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ... |
Artículo
Formally Verified Tableau-Based Reasoners for a Description Logic
(Springer, 2014)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ... |
Artículo
Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm
(Oxford Academic, 2013)
The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted ... |
Ponencia
Certified Symbolic Manipulation: Bivariate Simplicial Polynomials
(ACM, 2013)
Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ... |
Tesis Doctoral
Formalización en Isar de la metalógica de primer orden
(2012)
El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. ... |
Artículo
Formalization of a normalization theorem in simplicial topology
(Springer, 2012)
In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ... |
Artículo
Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
(Springer, 2011)
Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ... |
Ponencia
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
(Springer, 2011)
In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ... |
Ponencia
Sensorización y control de un proceso de mecanizado utilizando un sistema experto basado en reglas
(Asociación Española de Dirección e Ingeniería de Proyectos (AEIPRO), 2010)
Aunque el proceso de fabricación por arranque de viruta ha evolucionado mucho en los últimos años con la incorporación de ... |
Capítulo de Libro
Topología simplicial en ACL2
(Universidad de la Rioja, 2010)
|
Ponencia
Expert System to Real Time Control of Machining Processes
(Springer, 2009)
Industrial machining processes use automated milling machines. These machines are connected to a control device that ... |
Ponencia
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
(Springer, 2009)
Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It ... |
Artículo
Constructing Formally Verified Reasoners for the ALC Description Logic
(Elsevier, 2008)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ... |
Ponencia
KRRT: Knowledge Representation and Reasoning Tutor System
(Springer, 2007)
Knowledge Representation & Reasoning (KR&R) is a fundamental topic in Artificial Intelligence. A basic KR language is ... |
Ponencia
A Formally Verified Prover for the ALC Description Logic
(Springer, 2007)
The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ... |
Artículo
Foundational Challenges in Automated Data and Ontology Cleaning in the Semantic Web
(IEEE Computer Society, 2006)
The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the foundational ... |
Artículo
Formal Correctness of a Quadratic Unification Algorithm
(Springer, 2006)
We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ... |
Ponencia
Rete Algorithm Applied to Robotic Soccer
(Springer, 2005)
This article is a first approach to the use of Rete algorithm to design a team of robotic soccer playing agents for Robocup ... |
Artículo
Verification of the Formal Concept Analysis
(Real Academia de Ciencias, 2004)
This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ... |
Artículo
Formal verification of a generic framework to synthesize SAT-provers
(Springer, 2004)
We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability provers. ... |
Ponencia
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2
(Springer, 2003)
We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ... |
Ponencia
Formal Verification of Molecular Computational Models in ACL2: A Case Study
(Springer, 2003)
Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ... |
Ponencia
A Formal Proof of Dickson’s Lemma in ACL2
(Springer, 2003)
Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ... |
Ponencia
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.
(University of Texas, 2002)
In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ... |
Ponencia
Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT
(2002)
In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a ... |
Ponencia
Progress Report: Term Dags Using Stobjs
(University of Texas, 2002)
We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ... |
Artículo
Formal proofs about rewriting using ACL2
(Springer, 2002)
We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ... |
Ponencia
Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers
(Springer, 2002)
We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ... |
Ponencia
A Theory About First-Order Terms in ACL2
(University of Texas, 2002)
We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ... |
Capítulo de Libro
Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment
(Springer, 2002)
The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS ... |
Tesis Doctoral
 Teoría computacional (en ACL2) sobre cálculos proposicionales
(2002)
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. |
Ponencia
Verifying an Applicative ATP Using Multiset Relations
(Springer, 2001)
We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ... |
Ponencia
Multiset Relations: A Tool for Proving Termination
(University of Texas, 2000)
|
Ponencia
Formalizing Rewriting in the ACL2 Theorem Prover
(Springer, 2000)
We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ... |