Data

NameAlonso Jiménez, José Antonio
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

    56

  • Visits

    5363

  • Downloads

    9492

  Publications

 

Final Degree Project
Icon

Elementos de matemáticas formalizados en Isabelle/HOL

Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Núñez Fernández, Carlos (2020-01-01)
La finalidad de este trabajo es la formalización de teoremas de diferentes teorías de las matemáticas. Para ello, se han ...
Final Degree Project
Icon

Elementos de lógica formalizados en Isabelle/HOL

Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Santiago Fernández, Sofía (2020-01-01)
El objetivo de la Lógica es la formalización del conocimiento y su razonamiento. En este trabajo, estudiaremos elementos ...
Final Degree Project
Icon

Teoría de categorías y programación funcional

Alonso Jiménez, José Antonio; Pedraza López, Diego (2018-01-01)
En esencia, la teoría de categorías es el estudio de la composición. Una categoría es una colección de objetos y morfismos ...
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-01-01)
A detailed exposition of foundations of a logic-algebraic model for reasoning with knowledge bases speci ed by propositional ...
Final Degree Project
Icon

Matemática discreta en Haskell

Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Valverde Rodríguez, María Dolores (2017-06-01)
Discrete mathematics is characterized as the branch of mathematics dealing with finite and numerable sets. Concepts and ...
Final Degree Project
Icon

Lógica de primer orden en Haskell

Alonso Jiménez, José Antonio; Paluzo Hidalgo, Eduardo (2017-06-01)
This final degree project consists in the implementation of First Order Logic theory and algorithms in Haskell, a functional ...
Final Degree Project
Icon

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

Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Najarro Gómez, María (2016-06-01)
Formal Concept Analysis is a mathematical theory of data analysis with growing popularity across various domains such as ...
Final Degree Project
Icon

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

Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Rodríguez Chavarría, Daniel (2016-01-01)
The present paper aims to explain cryptography from the point of view of functional programming. In order to accomplish ...
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 ...
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

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

Sistema certificado de decisión proposicional basado en polinomios

Alonso Jiménez, José Antonio; Aranda Corral, Gonzalo A.; Borrego Díaz, Joaquín (Universidad de Sevilla, Departamento de Ciencias de la Computación e Inteligencia Artificial, 2009-01-01)
En [2] introducimos una regla de inferencia para la lógica proposicional (basado en el uso de la derivación de polinomios) ...
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-01-01)
We present a translation of problems of Formal Context Analysis into ideals problems in F2[x] through the Boolean ...
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. ...
PhD Thesis
Icon

Técnicas de depuración e integración de ontologías en el ámbito empresarial

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Paredes Moreno, Antonio (2007-01-01)
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 ...
Presentation
Icon

Ontology Cleaning by Mereotopological Reasoning

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Chávez González, Antonia María (IEEE Computer Society, 2004-01-01)
A mereotopological semantics to manage ontologies is presented. The aim is to provide a formal basis for ontology cleaning. ...
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

Verified Computer Algebra in ACL2 (Gröbner Bases Computation)

Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Alonso Jiménez, José Antonio; Ruiz Reina, José Luis (Springer, 2004-01-01)
In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner ...
Presentation
Icon

Towards a tool for ontology engineering

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Chávez González, Antonia María (IEEE Computer Society, 2004-01-01)
A tool based on a spatial representation of provisional ontologies is designed. The tool allows the cleming of Knowledge Bases, aa well to induce new concepts in early steps of the building of an ontology.
PhD Thesis
Icon

Verificación formal en ACL2 del Algoritmo de Buchberger

Alonso Jiménez, José Antonio; Ruiz-Reina, José-Luis; Medina Bulo, Inmaculada (2003-12-18)
En este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del ...
Presentation
Icon

Towards a Practical Argumentative Reasoning with Qualitative Spatial 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. (Springer, 2003-01-01)
Classical database management can be flawed if the Knowledge database is built within a complex Knowledge Domain. We ...
Presentation
Icon

Generalizing Programs via Subsumption

Gutiérrez Naranjo, Miguel Ángel; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín (Springer, 2003-01-01)
In this paper we present a class of operators for Machine Learning based on Logic Programming which represents a ...
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

Towards a Practical Argumentative Reasoning with Qualitative Spatial 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. (Springer, 2003-01-01)
Classical database management can be flawed if the Knowledge database is built within a complex Knowledge Domain. We ...
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 ...
PhD Thesis
Icon

Operadores de generalización para el aprendizaje clausal

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Gutiérrez Naranjo, Miguel Ángel (2002-01-01)
"En esta memoria hemos estudiado los procesos de generalización, el paso de lo particular a lo general, cuando la información ...
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-01-01)
The subsumption relation is crucial in the Machine Learning systems based on a clausal representation. In this paper we ...
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-01-01)
In environments with complex cognitive structure (such as semantic web or sophisticated spatial databases for geographical ...
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-01-01)
Este libro constituye el primer volumen de una serie sobre deducción automática. Su objetivo es la presentación de Prolog ...
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.
PhD Thesis
Icon

Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades

Alonso Jiménez, José Antonio; Ruiz Reina, José Luis (2001-01-01)
El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ...
Presentation
Icon

Proximidad entre cláusulas en programación lógica inductiva

Gutiérrez Naranjo, Miguel Ángel; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín (Universidad de Sevilla - Fundación El Monte, 2001-01-01)
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-01-01)
Presentation
Icon

A Certified Polynomial-Based Decision Procedure for Propositional Logic

Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Alonso Jiménez, José Antonio (Springer, 2001-01-01)
In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. ...
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

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-01-01)
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)
Presentation
Icon

Interpretación reactiva de sistemas basados en conocimiento.

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Pérez Jiménez, Mario de Jesús (Universidad de Granada, 1999-01-01)
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-01-01)
Todos los que hemos impartido tópicos diversos relativos a la Teoría de Conjuntos, en primer o segundo ciclo universitario, ...
PhD Thesis
Icon

Métodos algebraicos de razonamiento automático

Riscos Fernández, Agustín; Alonso Jiménez, José Antonio (1988-01-01)
Presentation
Icon

Preuve automatique dans le calcul propositionnel et les logiques trivalentes

Alonso Jiménez, José Antonio; Briales Morales, Emilio (1987-01-01)
Nous présentons une application des bases de Gröbner (bases standard) d’idéaux de polynômes la vérification des tautologies ...
Presentation
Icon

Lógicas polivalentes y bases de Gröbner

Alonso Jiménez, José Antonio (1987-01-01)
El objetivo de la comunicación es presentar una aplicación de las bases de Gröbner a la demostración automática en lógicas ...