• Trabajo Fin de Grado
      Icon

      Una introducción a la programación con conjuntos de respuesta. Aplicaciones 

      Jiménez Núñez, Marina (2022-06-22)
      The main objective of this paper is to present the answer set programming paradigm as a tool to model and solve combinatorial ...
    • Trabajo Fin de Grado
      Icon

      Lógica computacional desde el punto de vista de la programación funcional : eliminación de cuantificadores 

      Mateo Ceballos, María Dolores (2022-06-15)
      Computational Logic is a wide interdisciplinary field having its theoretical and practical roots in mathematics, computer ...
    • Trabajo Fin de Grado
      Icon

      Matemática discreta en Haskell 

      Valverde Rodríguez, María Dolores (2017-06)
      Discrete mathematics is characterized as the branch of mathematics dealing with finite and numerable sets. Concepts and ...
    • 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. ...
    • Trabajo Fin de Máster
      Icon

      Verificación formal de la lógica de Hoare en Isabelle/HOL 

      González Blanco, Natividad (2016-09)
      Hoare logic is a formal system developed by C.A.R. Hoare. This logic was introduced to verify formally imperative programs. ...
    • 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 ...
    • Artículo
      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)
      This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ...
    • Ponencia
      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)
      We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ...