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 researchers have proposed methods to parallelize the theorem proving process. Here, we use the massive parallelism of molecular reactions to implement parallel theorem provers. In particular, we show that the resolution refutation proof procedure can be naturally and efficiently implemented by DNA hybridization. Novel DNA encoding schemes, i.e. linear encoding and hairpin encoding, are presented and their effectiveness is verified by biochemical experiments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adleman, L., Molecular computation of solutions to combinatorial problems, Science, 266:1021–1024, 1994.
Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag New York Inc., 1942.
Hagiya, M., Arita, M., Kiga, D., Sakamoto, K., and Yokoyama, S., Towards parallel evaluation and learning of Boolean μ-formulas with molecules, Preliminary Proceedings of the Third DIMACS Workshop on DNA Based Computers, 105–114, 1997.
Hagiya, M., From molecular computing to molecular programming, Lecture Notes in Computer Science, 2001.
Hasegawa, R., Parallel theorem-proving system: MGTP, Proceedings of Fifth Generation Computer System, 1994.
Kobayashi, S., Horn clause computation with DNA molecules, Journal of Combinatorial Optimization, 3:277–299, 1999.
Lipton, R.J., DNA solution of hard computational problem, Science, 268:542–545, 1995.
Luger, G.F. and Stubblefield, W.A., Artificial Intelligence: Structures and Strategies for Complex Problem Solving, 2nd Ed., Benjamin/Cummings, 1993.
Lusk, E.L. and McCune, W.W., High-performance parallel theorem proving for shared-memory multiprocessors, http://wwwfp.mcs.anl.gov/~lusk/papers/roo/paper.html, 1998.
Mihalache, V., Prolog approach to DNA computing, Proceedings of the IEEE International Conference on Evolutionary Computation, IEEE Press, 249–254, 1997.
Nilsson, N.J., Aritificial Intelligence: A New Systhesis, Morgan Kaufman Publishers Inc., 1998.
Sa-Ardyen, P., Jonoska, N., and Seeman, N.C., Self-assembling DNA Graphs, Preliminary Proceedings of the Eighth International Meeting on DNA Based Computers, 20–28, 2002.
Sakamoto, K., Gouzu, H., Komiya, K., Kiga, D., Yokoyama, S., Yokomori, T., and Hagiya, M., Molecular computation by DNA hairpin formation, Science, 288:1223–1226, 2000.
Shin, S.-Y., Kim, D., Lee, I.-H., and Zhang, B.-T., Evolutionary sequence generation for reliable DNA computing, 2002 IEEE World Congress on Evolutionary Computation, 2002 (accepted).
Suttner, C., SPTHEO-A parallel theorem prover, Journal of Automated Reasoning, 18(2):253–258, 1997.
Uejima, H., Hagiya, M., and Kobayashi, S., Horn clause computation by selfassembly of DNA molecules, Preliminary Proceedings of the Seventh International Meeting on DNA Based Computers, 63–71, 2001.
Wasiewicz, P., Janczak, T., Mulawka, J.J., and Plucienniczak, A., The inference based on molecular computing, International Journal of Cybernetics and Systems, 31(3):283–315, 2000.
Winfree, E., Algorithmic self-assembly of DNA, Ph.D. Thesis, California Institute of Technology, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lee, IH., Park, JY., Jang, HM., Chai, YG., Zhang, BT. (2003). DNA Implementation of Theorem Proving with Resolution Refutation in Propositional Logic. In: Hagiya, M., Ohuchi, A. (eds) DNA Computing. DNA 2002. Lecture Notes in Computer Science, vol 2568. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36440-4_14
Download citation
DOI: https://doi.org/10.1007/3-540-36440-4_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00531-5
Online ISBN: 978-3-540-36440-5
eBook Packages: Springer Book Archive