| Paper ID | D6-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.
|
