Theorem Proving Based on Semantics of DNA Strand Graph

TL;DR

This paper explores how DNA computing can be used for automated theorem proving with resolution refutation, utilizing process calculus and strand graph semantics to model the computational process.

Contribution

It introduces a novel approach to theorem proving using DNA strand graph semantics, bridging DNA computing with formal logic proof methods.

Findings

DNA computing can implement resolution refutation for theorem proving

Process calculus and strand graph effectively model DNA-based proof processes

Demonstrates potential for DNA computing in formal logical reasoning

Abstract

Because of several technological limitations of traditional silicon based computing, for past few years a paradigm shift, from silicon to carbon, is occurring in computational world. DNA computing has been considered to be quite promising in solving computational and reasoning problems by using DNA strands. Resolution, an important aspect of automated theorem proving and mathematical logic, is a rule of inference which leads to proof by contradiction technique for sentences in propositional logic and first-order logic. This can also be called refutation theorem-proving. In this paper we have shown how the theorem proving with resolution refutation by DNA computation can be represented by the semantics of process calculus and strand graph.