论文部分内容阅读
清楚地叙述了自然推理系统中的存在量词消去规则和全称量词引入规则满足的条件，而这些条件在许多离散数学教科书中叙述得相当含糊。与某些教科书中存在量词消去规则只能用于无自由变元的公式不同，按照本文给出的条件，存在量词消去规则也可以用于有自由变元的公式，因而增强了系统的推理能力。引进了解释之间和赋值之间关于公式集的等价性，从而证明了系统是可靠的，即一个证明中的结论是其有提的逻辑推论．