Two Proof Procedures for a Cardinality Based Language in Propositional Calculus
Two Proof Procedures for a Cardinality Based Language in Propositional Calculus
复制标题
命题演算中基于基数的语言的两个证明过程
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
P. Siegel
中科院分区：
文献类型：
--
作者：
B. Benhamou;L. Sais;P. Siegel
本文利用势来提高命题演算的表达效率，并提高归结方法的效率。因此，为了表达命题问题和逻辑约束，我们引入了成对公式（ρ，ρ），这意味着“列表中的文字中至少ρ个文字为真”。这使得一个命题子句的一般化表达“至少有一个字面量是真的在那些子句”。我们提出了一个基数决议证明系统，我们证明了完整性和可判定性。给出了鸽子洞问题的一个线性证明，显示了基数的优点。
In this paper we use the cardinality to increase the expressiveness efficiency of propositional calculus and improve the efficiency of resolution methods. Hence to express propositional problems and logical constraints we introduce the pair formulas (ρ, ℒ) which mean that “at least ρ literals among those of a list ℒ are true”. This makes a generalization of propositional clauses which express ”At least one literal is true among those of the clause”. We propose a cardinality resolution proof system for which we prove both completenesss and decidability. A linear proof for Pigeon-hole problem is given in this system showing the advantage of cardinality.