| Molecular Computation Models in ACL2: a Simulation of Lipton's Experiment Solving SAT. # (2007) | |||||||||||||||
Abstract | |||||||||||||||
| 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. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||