All Dates/Times are Australian Eastern Standard Time (AEST)

Technical Program

Paper Detail

Paper IDD6-S5-T1.3
Paper Title An Automated Theorem Proving Framework for Information-Theoretic Results
Authors Cheuk Ting Li, The Chinese University of Hong Kong, Hong Kong SAR of China
Session D6-S5-T1: Information Inequalities II
Chaired Session: Monday, 19 July, 23:20 - 23:40
Engagement Session: Monday, 19 July, 23:40 - 00:00
Abstract We present a versatile automated theorem proving framework 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 capacity regions involving auxiliary random variables, automated deduction of properties of information-theoretic quantities (e.g. Wyner and G{\'a}cs-K{\"o}rner 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 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.