Abstract
Many fundamental theorems for Shannon’s entropy and Kolmogorov complexity can be formulated as linear inequalities (that is, inequalities for Shannon’s entropy of random variables or for Kolmogorov complexity of binary strings). Information inequalities have a wide range of applications in computer science, including problems of coding for communication networks and cryptography.There are several different mathematical techniques used to prove information inequalities. While the mathematical basis of these techniques is quite elaborate, the resulting inference rules are very simple and purely syntactical. The procedure of inference of new information inequalities can be formalized so that the proofs can be mechanically checked by a computer. Though the verification of a given proof is rather simple, the search for a new information inequality requires massive computations. The computational complexity of this problem can be reduced with several non-trivial and algorithmic techniques.In this work we systematize the exploitation of some known inference rules for information inequalities by developing a software assisting the inference and application of these inequalities, especially in the problems of secret sharing and hat guessing games. Although without the necessity of a computer, we also prove results in communication complexity of secret key agreement.