Theorem Proving Based on Semantics of DNA Strand Graph
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Review on DNA Strand Algebra and its Application
Several technological limitations of traditional silicon based computing are leading towards the paradigm shift, from silicon to carbon, in computational world. Among the unconventional modes of computing evolved in past…
Automated Theorem ProvingDNA Tweezers Based on Semantics of DNA Strand Graph
Because of the limitations of classical silicon based computational technology, several alternatives to traditional method in form of unconventional computing have been proposed. In this paper we will focus on DNA comput…
FormGraph Representations for Higher-Order Logic and Theorem Proving
This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem prove…
Automated Theorem ProvingA Theoretical Framework for Self-Play Theorem Proving Algorithms
Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) …
Contrastive LearningFormalizing Flag Algebras in Lean
Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-ch…