Browsing by Author 

Browsing by Author "Alonso Jiménez, José Antonio"  

Now showing items 1-20 of 57

    • Presentation
      Icon

      A Certified Polynomial-Based Decision Procedure for Propositional Logic 

      Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Alonso Jiménez, José Antonio (Springer, 2001)
      In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. ...
    • 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)
      Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...
    • 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)
      The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...
    • 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)
      In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...
    • Article
      Icon

      A logic-algebraic tool for reasoning with Knowledge-Based Systems 

      Alonso Jiménez, José Antonio; Aranda Corral, Gonzalo A.; Borrego Díaz, Joaquín; Fernández Lebrón, María Magdalena; Hidalgo Doblado, María José (Elsevier, 2018)
      A detailed exposition of foundations of a logic-algebraic model for reasoning with knowledge bases speci ed by propositional ...
    • Presentation
      Icon

      A methodology for the computer-aided cleaning of complex knowledge databases 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Chávez González, Antonia María; Gutiérrez Naranjo, Miguel Ángel; Navarro Marín, Jorge D. (IEEE Computer Society, 2002)
      In environments with complex cognitive structure (such as semantic web or sophisticated spatial databases for geographical ...
    • Presentation
      Icon

      A Quasi-Metric for Machine Learning 

      Gutiérrez Naranjo, Miguel Ángel; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín (Springer, 2002)
      The subsumption relation is crucial in the Machine Learning systems based on a clausal representation. In this paper we ...
    • 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)
      We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...
    • Presentation
      Icon

      A Topological Study of the Upward Refinement Operators on ILP 

      Gutiérrez Naranjo, Miguel Ángel; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín (CEUR-WS, 2000)
    • Final Degree Project
      Icon

      Análisis formal de conceptos desde el punto de vista de la programación funcional 

      Najarro Gómez, María (2016-06)
      Formal Concept Analysis is a mathematical theory of data analysis with growing popularity across various domains such as ...
    • 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)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...
    • Final Degree Project
      Icon

      Criptografía desde el punto de vista de la programación funcional 

      Rodríguez Chavarría, Daniel (2016)
      The present paper aims to explain cryptography from the point of view of functional programming. In order to accomplish ...
    • Book
      Icon

      Curso Práctico de Teoría de Conjuntos 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Pérez Jiménez, Mario de Jesús; Ruiz Reina, José Luis (Ediciones La Ñ, 1998)
      Todos los que hemos impartido tópicos diversos relativos a la Teoría de Conjuntos, en primer o segundo ciclo universitario, ...
    • Book
      Icon

      Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos) 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín (Kronos, 2002)
      Este libro constituye el primer volumen de una serie sobre deducción automática. Su objetivo es la presentación de Prolog ...
    • Presentation
      Icon

      Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Chávez González, Antonia María (Universidad de Sevilla - Fundación El Monte, 2001)
    • Final Degree Project
      Icon

      Elementos de lógica formalizados en Isabelle/HOL 

      Santiago Fernández, Sofía (2020)
      El objetivo de la Lógica es la formalización del conocimiento y su razonamiento. En este trabajo, estudiaremos elementos ...
    • Final Degree Project
      Icon

      Elementos de matemáticas formalizados en Isabelle/HOL 

      Núñez Fernández, Carlos (2020)
      La finalidad de este trabajo es la formalización de teoremas de diferentes teorías de las matemáticas. Para ello, se han ...
    • Presentation
      Icon

      Extending Attribute Exploration by Means of Boolean Derivatives 

      Alonso Jiménez, José Antonio; Aranda Corral, Gonzalo A.; Borrego Díaz, Joaquín; Fernández Lebrón, María Magdalena; Hidalgo Doblado, María José (CEUR-WS, 2008)
      We present a translation of problems of Formal Context Analysis into ideals problems in F2[x] through the Boolean ...
    • 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)
      We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...
    • 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)
      We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...