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, discovery of inner bounds in network information theory (in conjunction with the method by Lee and Chung), simplification of capacity regions involving auxiliary random variables, deduction of properties of information-theoretic quantities (e.g. Wyner and G\'acs-K\"orner common information), and 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 introduce the concept of existential information inequalities, which provides an axiomatic framework for a wide range of problems in information theory. To demonstrate the use of the framework, we present a new outer bound for the broadcast channel discovered by the framework.