Now showing items 1-20 of 29

    • Icon

      A Formal Proof of Dickson’s Lemma in ACL2  [Presentation]

      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 of polynomial ideals. In this case study, we present a formal proof of Dickson’s Lemma using the ...
    • Icon

      A Formally Verified Prover for the ALC Description Logic  [Presentation]

      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 family of logical formalisms for representing and reasoning about conceptual and terminological ...
    • Icon

      ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System  [Presentation]

      Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2009)
      Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows ...
    • Icon

      Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials  [Presentation]

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2011)
      In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain ...
    • Icon

      Certified Symbolic Manipulation: Bivariate Simplicial Polynomials  [Presentation]

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (ACM, 2013)
      Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In this paper, we focus on algebraic algorithms ...
    • Icon

      Constructing Formally Verified Reasoners for the ALC Description Logic  [Article]

      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. Recently, its importance has been increased since they are used as a basis for the Ontology Web Language ...
    • Icon

      Expert System to Real Time Control of Machining Processes  [Presentation]

      Martín Mateos, Francisco Jesús; González Valencia, Luis Carlos; Serrano Bello, Rafael (Springer, 2009)
      Industrial machining processes use automated milling machines. These machines are connected to a control device that provides the basic instructions used to obtain a piece. However, these processes depend on the human ...
    • Icon

      Formal Correctness of a Quadratic Unification Algorithm  [Article]

      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 receives as input two first-order terms and it returns a most general unifier of these terms if ...
    • Icon

      Formal proofs about rewriting using ACL2  [Article]

      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 and representation aspects of our work using the firstorder, quantifier-free logic of ACL2 and ...
    • Icon

      Formal Reasoning about Efficient Data Structures: A Case Study in ACL2  [Presentation]

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2003)
      We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms are represented as directed acyclic graphs (dags) and these graphs are stored in a single-threaded ...
    • Icon

      Formal verification of a generic framework to synthesize SAT-provers  [Article]

      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 provers. For that purpose, we develop a framework where we de ne a generic SAT-prover based on transformation ...
    • Icon

      Formal Verification of Molecular Computational Models in ACL2: A Case Study  [Presentation]

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the size of the problem, many methods to parallelize the process has been proposed. One of these ...
    • Icon

      Formalización en Isar de la metalógica de primer orden  [Doctoral Thesis]

      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. Más precisamente, formalizar en el sistema de razonamiento Isabelle/HOL/Isar la metateoría de la ...
    • Icon

      Formalization of a normalization theorem in simplicial topology  [Article]

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2012)
      In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, ...
    • Icon

      Formalizing Rewriting in the ACL2 Theorem Prover  [Presentation]

      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 seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation ...
    • Icon

      Formally Verified Tableau-Based Reasoners for a Description Logic  [Article]

      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 of the most basic description logics is ALC , used as a basis from which to obtain others. Description ...
    • Icon

      Foundational Challenges in Automated Data and Ontology Cleaning in the Semantic Web  [Article]

      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 foundational basis of cleaning agent design. The authors discuss some of them. They finally argue that ...
    • Icon

      KRRT: Knowledge Representation and Reasoning Tutor System  [Presentation]

      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 First– Order Logic (FOL), the most representative logic–based representation language, which is part ...
    • Icon

      Modelling algebraic structures and morphisms in ACL2  [Article]

      Heras, Jonathan; 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 provide a guide- line to implement a set of tools that facilitates the formalisations related ...
    • Icon

      Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT  [Presentation]

      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 first step to formalize unconventional models of computation in ACL2. As an application of this ...