- idUS
- Browsing by Author
Browsing by Author "Martín Mateos, Francisco Jesús"
Now showing items 21-40 of 43
-
Presentation
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)We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
-
Article
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)Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
-
Article
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)The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the ...
-
Presentation
KRRT: Knowledge Representation and Reasoning Tutor System
Alonso Jiménez, José Antonio; Aranda, Gonzalo A.; Martín Mateos, Francisco Jesús (Springer, 2007)Knowledge Representation & Reasoning (KR&R) is a fundamental topic in Artificial Intelligence. A basic KR language is ...
-
Final Degree Project
Librería Haskell sobre Model Checking
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
Librería sobre esteganografía en Haskell
Mariano Herzog, Teresa (2023-07)Steganography is the art of hiding the fact that comunication is taking place. In this project we present an introduction ...
-
Final Degree Project
Librería sobre grafos en Haskell : el problema del camino más corto
Manrique Merchán, Pablo (2023-07)The shortest path problem is an important problem in graph theory, consisting in finding paths between two nodes in ...
-
Article
Modelling algebraic structures and morphisms in ACL2
Heras, Jónathan; Martín Mateos, Francisco Jesús; Pascual, Vico (Springer, 2015)In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ...
-
Presentation
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)In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a ...
-
Presentation
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) -
Presentation
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)We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ...
-
Article
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)Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ...
-
Presentation
Rete Algorithm Applied to Robotic Soccer
Palomo, M.; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio (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 ...
-
Presentation
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)Aunque el proceso de fabricación por arranque de viruta ha evolucionado mucho en los últimos años con la incorporación ...
-
Chapter of Book
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)The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS ...
-
PhD Thesis
Teoría computacional (en ACL2) sobre cálculos proposicionales
Martín Mateos, Francisco Jesús (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.
-
Chapter of Book
Topología simplicial en ACL2
Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Universidad de la Rioja, 2010) -
Presentation
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) -
Presentation
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)We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...
-
Presentation
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)We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ...