命题逻辑中三元子句集的冗余文字

Redundant Literals of Ternary Clause Sets in Propositional Logic

自动推理是人工智能领域研究的核心问题之一。由于在基于归结的自动推理过程中会产生大量的冗余文字和冗余子句,进而影响归结自动推理的效率,因此消除子句集中的冗余文字和冗余子句具有重要的意义。在命题逻辑中,依据必需文字、有用文字、无用文字的相关概念和性质,针对部分三元子句集,分类给出这些三元子句集中冗余文字的判别方法,并通过具体实例对这些判别方法进行说明。

Automatic reasoning is one of the core issues in the field of artificial intelligence.Since a large number of redundant li-terals and redundant clauses are generated in the process of automatic reasoning based on resolution,the resolution efficiency will be affected.It is of great significance to eliminate redundant literals and redundant clauses in the clause set.In propositional logic,according to the related concepts and properties of necessary literals,useful literals and useless literals,this paper classifies and gives the judgment methods of redundant literals in some ternary clause sets,and explains these judgment methods through specific examples.