Mostrar el registro sencillo del ítem
Capítulo de Libro
Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment
dc.creator | Graciani Díaz, Carmen | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Pérez Jiménez, Mario de Jesús | es |
dc.date.accessioned | 2016-09-14T10:04:30Z | |
dc.date.available | 2016-09-14T10:04:30Z | |
dc.date.issued | 2002 | |
dc.identifier.isbn | 978-3-540-44311-7 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | http://hdl.handle.net/11441/44991 | |
dc.description.abstract | 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 proofs), we formalize the restricted model, based on DNA, due to L. Adleman. Also, we design a formal molecular program in this model that solves SAT following Lipton’s ideas.We prove using PVS the soundness and completeness ofthis molecular program. This work is intended to give an approach to the opportunities offered by mechanized analysis ofuncon ventional model ofcomputation in general. This approach opens up new possibilities ofv erifying molecular experiments before implementing them in a laboratory. | es |
dc.description.sponsorship | Ministerio de Educación y Cultura TIC2000-1368-C03-02 | |
dc.description.sponsorship | Ministerio de Educación y Cultura PB96-1345 | |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | Unconventional Models of Computation Volume 2509 of the series Lecture Notes in Computer Science pp 126-136 | es |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment | es |
dc.type | info:eu-repo/semantics/bookPart | 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.projectID | PB96-1345 | es |
dc.relation.publisherversion | http://link.springer.com/chapter/10.1007%2F3-540-45833-6_11 | es |
dc.identifier.doi | 10.1007/3-540-45833-6_11 | es |
dc.contributor.group | Universidad de Sevilla. TIC193: Computación Natural | |
idus.format.extent | 11 | es |
dc.publication.initialPage | 126 | es |
dc.publication.endPage | 136 | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.idus | https://idus.us.es/xmlui/handle/11441/44991 | |
dc.contributor.funder | Ministerio de Educación y Cultura (MEC). España |