Show simple item record

Chapter of Book

dc.creatorGraciani Díaz, Carmenes
dc.creatorMartín Mateos, Francisco Jesúses
dc.creatorPérez Jiménez, Mario de Jesúses
dc.date.accessioned2016-09-14T10:04:30Z
dc.date.available2016-09-14T10:04:30Z
dc.date.issued2002
dc.identifier.isbn978-3-540-44311-7es
dc.identifier.issn0302-9743es
dc.identifier.urihttp://hdl.handle.net/11441/44991
dc.description.abstractThe 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.sponsorshipMinisterio de Educación y Cultura TIC2000-1368-C03-02
dc.description.sponsorshipMinisterio de Educación y Cultura PB96-1345
dc.formatapplication/pdfes
dc.language.isoenges
dc.publisherSpringeres
dc.relation.ispartofUnconventional Models of Computation Volume 2509 of the series Lecture Notes in Computer Science pp 126-136es
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.titleSpecification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experimentes
dc.typeinfo:eu-repo/semantics/bookPartes
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.projectIDPB96-1345es
dc.relation.publisherversionhttp://link.springer.com/chapter/10.1007%2F3-540-45833-6_11es
dc.identifier.doi10.1007/3-540-45833-6_11es
dc.contributor.groupUniversidad de Sevilla. TIC193: Computación Natural
idus.format.extent11es
dc.publication.initialPage126es
dc.publication.endPage136es
dc.relation.publicationplaceBerlines
dc.identifier.idushttps://idus.us.es/xmlui/handle/11441/44991
dc.contributor.funderMinisterio de Educación y Cultura (MEC). España

FilesSizeFormatViewDescription
umc.pdf206.0KbIcon   [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