Dexter Kozen

The indefinite summation operator is like a discrete version of an indefinite integral. Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions defined on graphs, such as the Tutte, chromatic, flow, and reliability polynomials. These objects give a lot of interesting information about the graph, such as coloring information, but are intractable to compute in general. They can be produced in polynomial time for bounded treewidth graphs, but the traditional combinatorial algorithms are still very inefficient, and we were led to investigate symbolic algorithms. To do this, we needed to develop the algebraic properties of the indefinite summation operator and the generalized Kronecker delta from an axiomatic viewpoint. Our main result is a complete axiomatization of the equational theory of these constructs; that is, all equations that hold under the intended interpretations are derivable in the calculus. The completeness proof uses some basic notions from algebraic geometry.

Monday, September 17, 2007 4:00 PM 5130 Upson Hall		Theory Seminar Fall 2007 CS 789
	Dexter Kozen Cornell University
	Indefinite Summation and the Kronecker Delta
	The indefinite summation operator is like a discrete version of an indefinite integral. Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions defined on graphs, such as the Tutte, chromatic, flow, and reliability polynomials. These objects give a lot of interesting information about the graph, such as coloring information, but are intractable to compute in general. They can be produced in polynomial time for bounded treewidth graphs, but the traditional combinatorial algorithms are still very inefficient, and we were led to investigate symbolic algorithms. To do this, we needed to develop the algebraic properties of the indefinite summation operator and the generalized Kronecker delta from an axiomatic viewpoint. Our main result is a complete axiomatization of the equational theory of these constructs; that is, all equations that hold under the intended interpretations are derivable in the calculus. The completeness proof uses some basic notions from algebraic geometry.