A DNA-based Theorem Proving by Resolution Refutation
Ji-Yoon Park1, In-Hee Lee2, Young-Gyu Chai, Byoung-Tak Zhang
1scolaswhite@hotmail.com, Dept. of Biochemistry and Moleluar Biology, Hanyang University; 2ihlee@bi.snu.ac.kr, Biointelligence Laboratory School of Computer Science and Engineering, Seoul National University
Theorem proving is a method of automated reasoning. In theorem proving, one must decide methods for representing information and inference rules for drawing conclusions. It has a broad range of applications involving diagnosis and decision-making. Resolution refutation used to prove the evidence of theorem proving. But, theorem proving by resolution refutation has a difficulty in actual condition. The time of theorem proving increases exponentially with the complex or the number of axioms. The drawbacks of theorem proving were improved by parallel theorem provers. Here, we used the massive parallelism of molecular reactions to implement parallel theorem provers. We also proposed a encoding for logical formulas and presented resolution refutation process by DNA hybridization reaction. Resolution of a variable between each clause is represented by the hybridization of two regions corresponding to that literal in each clause. These DNA hybridization makes in a natural way to perform massive parallelism. Finally, the resulting product was examined by gel electrophoresis.