dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-10T11:24:58Z | |
dc.date.available | 2019-05-10T11:24:58Z | |
dc.date.issued | 2003 | |
dc.identifier.citation | Martí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.isbn | 978-3-540-22218-7 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86270 | |
dc.description.abstract | 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 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.sponsorship | Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | TTIA 2003: 5th Conference on Technology Transfer (2003), p 344-353 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Formal Verification of Molecular Computational Models in ACL2: A Case Study | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | TIC2000-1368-C03-02 | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-540-25945-9_34 | es |
dc.identifier.doi | 10.1007/978-3-540-25945-9_34 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 10 | es |
dc.publication.initialPage | 344 | es |
dc.publication.endPage | 353 | es |
dc.eventtitle | TTIA 2003: 5th Conference on Technology Transfer | es |
dc.eventinstitution | San Sebastian, España | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.sisius | 6515161 | es |