Repositorio de producción científica de la Universidad de Sevilla

Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment

Opened Access Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment

Citas

buscar en

Estadísticas
Icon
Exportar a
Autor: Graciani Díaz, Carmen
Martín Mateos, Francisco Jesús
Pérez Jiménez, Mario de Jesús
Departamento: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Fecha: 2002
Publicado en: Unconventional Models of Computation Volume 2509 of the series Lecture Notes in Computer Science pp 126-136
ISBN/ISSN: 978-3-540-44311-7
Tipo de documento: Capítulo de Libro
Resumen: 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.
Tamaño: 206.0Kb
Formato: PDF

URI: http://hdl.handle.net/11441/44991

DOI: 10.1007/3-540-45833-6_11

Ver versión del editor

Mostrar el registro completo del ítem


Esta obra está bajo una Licencia Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 Internacional

Este registro aparece en las siguientes colecciones