Ligation module for in-vitro selection in DNA computing

In this paper a classical AI problem is proposed to be solved by DNA computing: theorem proving. Since the complexity grows exponentially with the size of the problem, the solving process should be done in parallel. Massive parallelism is one of the advantages of DNA computers. It will be shown that the resolution refutation proof can be readily implemented by DNA hybridisation and ligation. Microreactors lend themselves to a relatively simple implementation of DNA computing. Not only is the design of the DNA critical for the success of the system but also the architecture of the microfluidic structure. Here the DNA performs the computation, while the microfluidics aids the biochemical steps necessary to manipulate the DNA, i.e. hybridisation and ligation.