Listar por autor 

Listar por autor "Martín Mateos, Francisco Jesús"                

Mostrando ítems 21-40 de 43

    • Ponencia
      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)
      We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
    • Artículo
      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)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
    • Artículo
      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)
      The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the ...
    • Ponencia
      Icon

      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 ...
    • Trabajo Fin de Grado
      Icon

      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 ...
    • Trabajo Fin de Grado
      Icon

      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 ...
    • Trabajo Fin de Grado
      Icon

      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 ...
    • Artículo
      Icon

      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 ...
    • Ponencia
      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)
      In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a ...
    • Ponencia
      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)
    • Ponencia
      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)
      We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ...
    • Artículo
      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)
      Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ...
    • Ponencia
      Icon

      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 ...
    • Ponencia
      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)
      Aunque el proceso de fabricación por arranque de viruta ha evolucionado mucho en los últimos años con la incorporación ...
    • Capítulo de Libro
      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)
      The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS ...
    • Tesis Doctoral
      IconIcon

      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.
    • Capítulo de Libro
      Icon

      Topología simplicial en ACL2 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Universidad de la Rioja, 2010)
    • Ponencia
      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)
    • Ponencia
      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)
      We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...
    • Ponencia
      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)
      We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ...