DNA Implementation of Theorem Proving with Resolution Refutation in Propositional Logic

Autor:	Haeman Jang, Byoung-Tak Zhang, Young Gyu Chai, In-Hee Lee, Ji-Yoon Park
Rok vydání:	2003
Předmět:	Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Proof complexity Second-order logic Compactness theorem Gap theorem Resolution (logic) Proof procedure Algorithm First-order logic Mathematics
Zdroj:	DNA Computing ISBN: 9783540005315 DNA
DOI:	10.1007/3-540-36440-4_14
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::b6a4f9152e8dd16ba81c799d251cd9bb https://doi.org/10.1007/3-540-36440-4_14 Zobrazit plný text záznamu