An Automated Theorem Proving Framework for Information-Theoretic Results

We present a versatile automated theorem proving framework which is capable of automated proofs of outer bounds in network information theory, automated discovery of inner bounds in network information theory (in conjunction with the method by Lee and Chung), simplification of expressions and capacity regions, automated deduction of properties of information-theoretic quantities (e.g. Wyner and G\'acs-K\"orner common information), and automated discovery of non-Shannon-type inequalities, under a unified framework. Our method is based on the linear programming approach for proving Shannon-type information inequalities studied by Yeung and Zhang, together with a novel pruning method for searching auxiliary random variables. We also introduce the concept of existential information inequalities, which provides an axiomatic framework for a wide range of problems in information theory.