- idUS
- Investigación
- Ingeniería y Arquitectura
- Ciencias de la Computación e Inteligencia Artificial
- Artículos (Ciencias de la Computación e Inteligencia Artificial)
- Listar Artículos (Ciencias de la Computación e Inteligencia Artificial) por autor
Listar Artículos (Ciencias de la Computación e Inteligencia Artificial) por autor "Alonso Jiménez, José Antonio"
Mostrando ítems 1-10 de 10
-
Ponencia
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 ...
-
Artículo
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 ...
-
Artículo
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. ...
-
Artículo
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 ...
-
Artículo
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 ...
-
Artículo
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)We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability ...
-
Artículo
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
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 ...
-
Artículo
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. ...
-
Artículo
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)This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ...