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

Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT

Opened Access Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT
Estadísticas
Icon
Exportar a
Autor: Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio
Pérez Jiménez, Mario de Jesús
Sancho Caparrini, Fernando
Departamento: Universidad de sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Fecha: 2002
Publicado en: Third International Workshop on the ACL2 Theorem Prover and Its Applications (2002), p 175-187
Tipo de documento: Ponencia
Resumen: In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a first step to formalize unconventional models of computation in ACL2. As an application of this model, an implementation of Lipton’s experiment solving SAT [7] is described, based on the formalization given in [6]. We use ACL2 to make a formal proof of the completeness and soundness properties of the function implementing the experiment
Cita: Martín Mateos, F.J., Alonso Jiménez, J.A., Pérez Jiménez, M.d.J. y Sancho Caparrini, F. (2002). Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT. Recuperado de
Tamaño: 195.1Kb
Formato: PDF

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

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