Molecular Theorem Proving for MicroRNA Module Detection


DNA computing is a form of computing which solves computational problems with DNA and standard molecular biological techniques, utilizing the powerful and precise molecular recognition affinity to form base pairs between nucleic acids. This new concept of computing has been able to solve 20-variable satisfiability problem, to construct DNA nanostructure by self-assembly, to implement blocked cellular automata by self-assembling DNA tiles, to operate logic gates and to construct DNA Boolean circuit, etc. after Adleman’s traveling salesman problem solving. In the development of aptamer based-DNA nanodevice and autonomous molecular machine, a set of active biological small molecules are used as input data and logic elements for solving or control molecular problems. Along with these works, we applied a DNA computing method that can detect multiple miRNAs.

Schematic of a proposed system. (A) A simple set of clauses is designed to identify the presence of molecules ‘X1’ and ‘X2’. A1 ∨ B1 and A2 ∨ B2 are clauses for ‘X1’ and ‘X2’, and D is a set of logical elements. (B) The hybridization form of molecule ‘X1’ and ‘X2’ is simplified based on the formula in Fig. 1A for in vitro computing. The yellow circle indicates thiol group modification for Au-NP conjugation. To identify two data sequences (X1, X2), total 6 other logic elements are designed. The negation symbol ‘ ┓’ indicates complimentary sequences in a case of nucleic acids. (C) The proof of unsatisfiability of the CNF formula composed of the clauses in (A) by resolution. An empty clause is derived through resolution among input clauses. (D) By applying Au-NPs and thiol-modified DNA sequences, in silico resolution can be executed in vitro environment. DNA clauses designed based on the formula are self-assembled by complementarity what is called molecular computing process in out system. And, a molecular computing result indicating ‘presence’ is distinguished by colorimetric changes derived from the formation of large DNA-linked three-dimensional aggregates.


  • Lee, I.-H., Park, J.-Y., Jang, H.-M., Chai, Y.-G., and Zhang, B.-T. (2003) DNA implementation of theorem proving with resolution refutation in propositional logic, Lecture Notes in Computer Science, 2568:156-167
  • Lee, I.-H., Lee, J.-H., Yang, K.A., Lee, J. H., Chai, Y.-G., Zhang, B.-T. (2006) Massively parallel logical computation by self-Assembly of DNA-linked nanoparticles. Nano Korea 2006, Ilsan, Korea
  • Yang K.A., Lee, J.-H., Lee, I.-H., Zhang, B.-T. (2007) A multiple microRNA detection system based on computational self-assembly of DNA-gold nanoparticles. FNANO 2007. (Accepted)
  • Kim, J.S., Lee, J.-W., Noh, Y.-K., Park, J.-Y., Lee, D.-Y., Chai, Y.-G., Kim, J.-C., Zhang, B.-T. (2007) An evolutionary Monte Carlo algorithm for predicting DNA hybridization. Biosystems (In press)

Project Title Molecular Theorem Proving for MicroRNA Module Detection
Sponsor The Ministry of Industry and Commerce
Principal Investigator Prof.Byoung-Tak Zhang
Researchers In-Hee Lee
Kyung-Ae Yang
Ji-Hoon Lee
Duration 2002 - 2007
Cooperative Research Institutes 나노응용시스템연구센터
서울대학교 세포 및 미생물공학 연구실

Contact Je-Hwan Ryu
E-Mail jhryu(at)
Phone +82-2-880-9131
Fax +82-2-880-9131