Martín-Mateos, F. J., Pérez-Jiménez M. J., & Sancho-Caparrini F.  (2002).??Molecular Computation Models in ACL2: A Simulation of Lipton's SAT Experiment in the  Adleman's Restricted Model.  Third International Workshop on the ACL2 Theorem Prover and its Applications.  175-187.