Two proof procedures for a cardinality based language in propositional calculus

Abstract

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 (ρ, L) which mean that “at least ρ literals among those of a list L 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. On other hand we provide an enumerative method (DPC) which is Davis and Putnam procedure adapted with Cardinality. Good results are obtained on many known problems such as Pigeon-hole problem, Queenes and some other instances derived from mathematical theorems (Ramsey, Schur's lemma) when this method is augmented with the principle of symmetry.