中间逻辑中的范式研究

论文摘要

中间逻辑是强弱介于经典逻辑与直觉主义逻辑之间的一大类命题逻辑。近年来，这些逻辑在计算机科学领域中受到极大的重视。而范式在逻辑及其相关领域中起着很重要的作用，特别是对于自动定理证明、自动推理和逻辑程序领域。本论文的主要目的是：寻找一些可以应用到基于中间逻辑的自动定理证明、自动推理和逻辑程序等领域的有用范式；研究这些范式在各中间逻辑中的存在性；设计一些用来对公式进行以上范式化简的算法。在本论文中，我们深入地研究了中间逻辑中的范式问题。共涉及到六种范式，包括：蕴含范式、扩展合取与析取范式、弱合取、析取与蕴含范式。我们证明了HT逻辑是唯一的具有蕴含范式的非经典中间逻辑，同时研究了三种弱范式在G(?)del逻辑中的存在性。对于公式的范式化简，我们提出了两类范式化简算法，一类是基于模型刻画公式的语义方法，另一类是基于重写系统的语法方法。作为以上研究的附加结果，我们得到了四种模型刻画公式，引入了Kripke模型之间初等蕴含的概念，并给出了一个初等蕴含的充分必要条件。最后，我们研究了关于以上范式化简问题的复杂性。

论文目录

• 摘要
• Abstract
• 1 Introduction
• 1.1 . Background
• 1.2 Main Results
• 1.3 Contents
• 2 Logics and Semantics
• 2.1 Intermediate Logics
• 2.2 Kripke Semantics
• 2.3 Go|¨del Logics
• 3 Normal Forms and Their Existence
• 3.1 Normal Forms
• 3.2 Model-Characterizing Formulas
• 3.2.1 Conjunctive Model-Characterizing Formulas
• 3.2.2 Disjunctive Model-Characterizing Formulas
• 3.3 Existence of Normal Forms
• 3.4 Weakest Logics with Normal Forms
• 4 Normal Form Reductions
• 4.1 Semantical Reductions
• 4.2 Syntactical Reductions
• 4.2.1 Syntactical WCNF-Reduction
• 4.2.2 Syntactical WINF-Reduction
• 4.3 Computational Complexity
• 5 Conclusions and Further Work
• Acknowledgements
• Bibliography
• 在学期间在省级以上刊物发表的论文目录
• 在学期间参加的科研项目