对偶直觉主义逻辑(DJ)一般是通过,在直觉主义逻辑的基础上,用蕴涵的对偶算子(-)替换直觉主义蕴涵算子(→)得到。关于DJ的研究,前人做了许多探索。这些不同探索可以主要分为语义和语法两方面。在语义方面,Rauszer在直觉主义逻辑的基础上加对偶算子得到BH逻辑(也称BiInt),得到对偶的代数语义和对偶的克里普克语义；Goodman用代数的方法研究了对偶直觉主义逻辑的语义。语法方面,Rauszer, Urbas, Czemark, Goodman等人,分别给出了对偶直觉主义逻辑的序列演算系统(LDJ)。Gore研究了对偶直觉主义逻辑的display演算。Luca Tranchini则给出了对偶直觉主义逻辑的自然演绎系统(NDJ)。1980年维瑟最早提出基本命题逻辑(BPL)的自然演绎系统,并规定框架为传递框架,给出了BPL的克里普克语义,且证明了在传递框架下的具有可靠性和完全性,证明了演绎定理。之后一些学者从希尔伯特式公理系统,根岑式序列演算系统,代数语义等方面对它进行了研究。对直觉主义命题逻辑的子逻辑——基本命题逻辑而言,其对偶的基本命题逻辑(DBPL)及其自然演绎系统(NDB)尚无人研究。因此,本人主要从以下几个方面对其进行研究：第一部分为文献综述,通过回顾历史,整理与整篇论文相关的前人的研究成果,得到整篇论文的知识线索。第二部分为研究背景,介绍了对偶直觉主义命题逻辑的自然演绎系统NDJ。这一章主要分为内容上逐层深入的三个部分,相继介绍了直觉主义逻辑Int、对偶直觉主义逻辑DJ、对偶直觉主义逻辑的自然演绎系统NDJ。第三部分为研究背景,介绍了基本命题逻辑BPL的自然演绎系统。这一章从语言、语义、自然演绎系统、逻辑性质、哲学意义和其他重要结论对BPL进行了介绍。第四部分为论文研究的主要内容,作者对对偶基本命题逻辑DBPL的自然演绎系统进行了研究,主要给出了DBPL的语言语义、自然演绎系统、并且证明了该系统具有可靠性和一些其他重要结论。第五部分为结论和总结。这一章是本文研究结论和创新点的总结,提出了对未来的展望。