DNA implementation of theorem proving with resolution refutation in propositional logic

Abstract

Abstract.Theorem proving is a classical AI problem having a broad range of applications.Since its complexity grows exponentially with the size of the problem,many esearchers have proposed methods to par- allelize the theorem proving process.In this paper,we use the massive parallelism of molecular reactions to implement parallel theorem provers. In particular,we show that the resolution efutation proof procedure can be naturally and e ciently implemented by DNA hybridization.Novel DNA encoding schemes,i.e.linear encoding and hairpin encoding,are presented and their e ectiveness is veri ed by bio-lab experiments.