Ponencia
Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT
Autor/es | 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 de publicación | 2002 |
Fecha de depósito | 2016-09-13 |
Publicado en |
|
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 ... 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 |
Agencias financiadoras | Ministerio de Ciencia y Tecnología (MCYT). España |
Identificador del proyecto | TIC2000-1368-CO3-02 |
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 |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
2002-ACL2-Adleman.pdf | 195.1Kb | [PDF] | Ver/ | |