• Artículo
      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)
      We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...
    • Ponencia
      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)
      We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...
    • Artículo
      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)
      We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability ...
    • Ponencia
      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)
      Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...
    • Ponencia
      Icon

      Formal Verification of P Systems with Active Membranes through Model Checking 

      Ipate, Florentin; Lefticaru, Raluca; Pérez Hurtado de Mendoza, Ignacio; Pérez Jiménez, Mario de Jesús; Tudose, Cristina (Springer, 2011)
      Formal verification of P systems using model checking has attracted a significant amount of research in recent years. ...
    • Capítulo de Libro
      Icon

      Formal Verification of Programs in Molecular Models with Random Access Memory 

      Pérez Jiménez, Mario de Jesús; Sancho Caparrini, Fernando (Fénix Editorial, 2005)
      Formal verification of molecular programs is a first step towards their automatic processing by means of reasoning ...
    • Tesis Doctoral
      Icon

      Formalización en Isar de la metalógica de primer orden 

      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. ...
    • Artículo
      Icon

      Formalization of a normalization theorem in simplicial topology 

      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 ...
    • Ponencia
      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)
      We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
    • Artículo
      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)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
    • Ponencia
      Icon

      Forward and Backward Chaining with P Systems 

      Ivanov, Sergiu; Alhazov, Artiom; Rogozhin, Vladimir; Gutiérrez Naranjo, Miguel Ángel (Fénix Editora, 2011)
      On the one hand, one of the concepts which lies at the basis of membrane computing is the multiset rewriting rule. On the ...
    • Artículo
      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)
      The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the ...
    • Ponencia
      Icon

      Four (Somewhat Nonstandard) Research Topics 

      Paun, Gheorghe (Fénix Editora, 2014)
      Four research directions are suggested, dealing with the following four main ideas: computing along the axon (up to now, ...
    • Ponencia
      Icon

      FPGA Implementation of Robot Obstacle Avoidance Controller based on Enzymatic Numerical P Systems 

      Shang, Zeyi; Verlan, Sergey; Zhang, Gexiang; Pérez Hurtado de Mendoza, Ignacio (IMCS: International Membrane Computing Society, 2019)
      It is a long-cherished wish to implement numerical P systems (NPS) on a parallel architecture so that its large scale ...
    • Ponencia
      Icon

      Fractals and P Systems 

      Gutiérrez Naranjo, Miguel Ángel; Pérez Jiménez, Mario de Jesús (Fénix Editora, 2006)
      In this paper we show that the massive parallelism, the synchronous appli- cation of the rules, and the discrete nature ...
    • Artículo
      Icon

      Fragments of Arithmetic and true sentences 

      Cordón Franco, Andrés; Fernández Margarit, Alejandro; Lara Martín, Francisco Félix (Wiley, 2005)
      By a theorem of R. Kaye, J. Paris and C. Dimitracopoulos, the class of the ¦n+1–sentences true in the standard model is ...
    • Ponencia
      Icon

      Un Framework para Big Data Optimization Basado en jMetal y Spark 

      Barba González, Cristóbal; Nebro, Antonio J.; García Nieto, José Manuel; Cordero, José A.; Durillo, Juan J.; Navas Delgado, Ismael; Aldana Montes, José F. (Universidad de Salamanca, 2016)
      Las metaheur sticas multi-objetivo se han convertido en t ecnicas muy utilizadas para la resoluci on problemas complejos ...
    • Artículo
      Icon

      From distribution to replication in cooperative systems with active membranes: A frontier of the efficiency 

      Valencia Cabrera, Luis; Orellana Martín, David; Martínez del Amor, Miguel Ángel; Riscos Núñez, Agustín; Pérez Jiménez, Mario de Jesús (Elsevier, 2018)
      P systems with active membranes use evolution, communication, dissolution and division(or separation) rules. They do not ...
    • Artículo
      Icon

      From fault detection to one-class severity discrimination of 3D printers with one-class support vector machine 

      Li, Chuan; Cabrera, Diego; Sancho Caparrini, Fernando; Cerrada, Mariela; Sánchez, René-Vinicio; Estupinan, Edgar (Elsevier, 2021)
      The lack of faulty condition data reduces the feasibility of supervised learning for fault detection or fault severity ...
    • Artículo
      Icon

      From NP-Completeness to DP-Completeness: A Membrane Computing Perspective 

      Valencia Cabrera, Luis; Orellana Martín, David; Martínez del Amor, Miguel Ángel; Pérez Hurtado de Mendoza, Ignacio; Pérez Jiménez, Mario de Jesús (Hindawi, 2020)
      Presumably efficient computing models are characterized by their capability to provide polynomial-time solutions for ...