A Study of Operations Research Solutions Techniques in Combinatorial Problem towards Constraint Programming

Formalizing combinatorial arguments using operational properties

Abstract

Many numerical identities are proved applying clever but informal combinatorial arguments. A formal representation is presented to prove these identities closely following these arguments. The main formal tool used to that end is, operationally, an abstract and axiomatic generalization of the Sigma notation (Σ), which is utilized for expressing and manipulating summations and counts. Operational properties are provided with algebraic properties that make it possible to perform different naturally important operations. In this paper we present a formal version and some more examples that show how to practically interpret combinatorial arguments used in literature. We present typical combinatorial evidence of the inclusion-exclusion theorem. Combinatory evidence of numerical identity is either that both sides of the given equation count the very same kinds of objects in two different ways or show a bijection between the sets that show up on each side of the equation. The two expressions must therefore be the same. The dream most combinatorialists make when they prove their identity is this kind of argument. Such arguments are generally informal and, it is likely to be safe to say, ad hoc, without a unified formal basis.