Show simple item record

dc.creatorMartín Mateos, Francisco Jesúses
dc.creatorAlonso Jiménez, José Antonioes
dc.creatorHidalgo Doblado, María Josées
dc.creatorRuiz Reina, José Luises
dc.date.accessioned2019-05-10T11:24:58Z
dc.date.available2019-05-10T11:24:58Z
dc.date.issued2003
dc.identifier.citationMartín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2003). Formal Verification of Molecular Computational Models in ACL2: A Case Study. En TTIA 2003: 5th Conference on Technology Transfer (344-353), San Sebastian, España: Springer.
dc.identifier.isbn978-3-540-22218-7es
dc.identifier.issn0302-9743es
dc.identifier.urihttps://hdl.handle.net/11441/86270
dc.description.abstractTheorem 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 approaches is based on the massive parallelism of molecular reactions. ACL2 is an automated theorem prover especially adequate for algorithm verification. In this paper we present an ACL2 formalization of a molecular computational model: Adleman’s restricted model. As an application of this model, an implementation of Lipton’s experiment solving SAT is described. We use ACL2 to make a formal proof of the completeness and soundness properties of this implementation.es
dc.description.sponsorshipMinisterio de Ciencia y Tecnología TIC2000-1368-C03-02es
dc.formatapplication/pdfes
dc.language.isoenges
dc.publisherSpringeres
dc.relation.ispartofTTIA 2003: 5th Conference on Technology Transfer (2003), p 344-353
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.titleFormal Verification of Molecular Computational Models in ACL2: A Case Studyes
dc.typeinfo:eu-repo/semantics/conferenceObjectes
dc.type.versioninfo:eu-repo/semantics/submittedVersiones
dc.rights.accessrightsinfo:eu-repo/semantics/openAccesses
dc.contributor.affiliationUniversidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificiales
dc.relation.projectIDTIC2000-1368-C03-02es
dc.relation.publisherversionhttps://link.springer.com/chapter/10.1007/978-3-540-25945-9_34es
dc.identifier.doi10.1007/978-3-540-25945-9_34es
dc.contributor.groupUniversidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimientoes
idus.format.extent10es
dc.publication.initialPage344es
dc.publication.endPage353es
dc.eventtitleTTIA 2003: 5th Conference on Technology Transferes
dc.eventinstitutionSan Sebastian, Españaes
dc.relation.publicationplaceBerlines
dc.identifier.sisius6515161es

FilesSizeFormatViewDescription
Formal Verification of Molecular ...292.2KbIcon   [PDF] View/Open  

This item appears in the following collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Except where otherwise noted, this item's license is described as: Attribution-NonCommercial-NoDerivatives 4.0 Internacional