Inequalities on submodular functions via term rewriting

•We devise a method for proving inequalities on submodular functions.•We prove several inequalities using our method.•As applications, we analyze several algorithms for submodular maximization.

We devise a method for proving inequalities on submodular functions, with a term rewriting flavor. Our method comprises of the following steps: (1) start with a linear combination X   of the values of the function; (2) define a set of simplification rules; (3) conclude that X⩾YX⩾Y, where Y is a linear combination of a small number of terms which cannot be simplified further; (4) calculate the coefficients of Y by evaluating X and Y on functions on which the inequality is tight.The crucial third step is non-constructive, since it uses compactness of the dual cone of submodular functions. Its proof uses the classical uncrossing technique with a quadratic potential function. We prove several inequalities using our method, and use them to tightly analyze the performance of two natural (but non-optimal) algorithms for submodular maximization, the random set algorithm and local search.