Now showing items 21-29 of 29

    • IconProof Pearl: a Formal Proof of Higman’s Lemma in ACL2  [Article]

      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. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. ...
    • IconRete Algorithm Applied to Robotic Soccer  [Presentation]

      Palomo, M.; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio (Springer, 2005)
      This article is a first approach to the use of Rete algorithm to design a team of robotic soccer playing agents for Robocup Soccer Server. Rete algorithm is widely used to design rule-based expert systems. Robocup Soccer ...
    • IconSpecification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment  [Chapter of Book]

      Graciani Díaz, Carmen; Martín Mateos, Francisco Jesús; Pérez Jiménez, Mario de Jesús (Springer, 2002)
      The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS verification system (an interactive environment for writing formal specifications and checking formal ...
    • IconTeoría computacional (en ACL2) sobre cálculos proposicionales  [Doctoral Thesis]

      Martín Mateos, Francisco Jesús (2002)
      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.
    • IconUsing Abstract Stobjs in ACL2 to Compute Matrix Normal Forms  [Presentation]

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2017)
      We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define a formally verified algorithm that given a matrix with elements in the ring of integers, computes ...
    • IconVerification in ACL2 of a Generic Framework to Synthesize SAT–Provers  [Presentation]

      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 purpose, we present a framework where we define a generic transformation based SAT–prover, and ...
    • IconVerification of the Formal Concept Analysis  [Article]

      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 represent and formally verify some algorithms of this theory. We also develop a method to transform ...
    • IconVerifying an Applicative ATP Using Multiset Relations  [Presentation]

      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 can be used to mechanically prove non-trivial termination properties. Every relation on a set A ...
    • IconVerifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm  [Article]

      Lambán Pardo, Laureano; Rubio, Julio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Oxford Academic, 2013)
      The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying ...