This paper is on developing some computer-assisted proof methods involving non-classical inequalities for Shannon entropy. Two areas of the applications of information inequalities are studied: Secret sharing schemes and hat guessing games. In the former a random secret value is transformed into shares distributed among several participants in such a way that only the qualified groups of participants can recover the secret value. In the latter each participant is assigned a hat colour and they try to guess theirs while seeing only some of the others'. The aim is to maximize the probability that every player guesses correctly, the optimal probability depends on the underlying sight graph. We use for both problems the method of non-Shannon-type information inequalities going back to Z. Zhang and R. W. Yeung. We employ the linear programming technique that allows to apply new information inequalities indirectly, without even writing them down explicitly. To reduce the complexity of the problems of linear programming involved in the bounds we extensively use symmetry considerations. Using these tools, we improve lower bounds on the ratio of key size to secret size for the former problem and an upper bound for one of the ten vertex graphs related to an open question by Riis for the latter problem.

翻译：本文旨在开发一种涉及香农熵的非经典不等式的计算机辅助证明方法。研究了信息不等式在两个领域的应用：秘密共享方案和帽子猜测游戏。在前者中，随机秘密值被转换为份额并分配给若干参与者，使得只有特定参与者群体才能恢复秘密值。在后者中，每位参与者被分配一种帽子颜色，他们仅能看到其他部分参与者的帽子颜色，并尝试猜测自己的帽子颜色。目标是最大化所有玩家正确猜测的概率，该最优概率取决于底层可见图。针对这两个问题，我们使用了可追溯至Z. Zhang和R. W. Yeung的非香农型信息不等式方法。我们采用了线性规划技术，该技术能够间接应用新的信息不等式，甚至无需显式写出这些不等式。为降低问题中相关线性规划边界的复杂度，我们广泛利用了对称性考量。借助这些工具，我们改进了前一个问题中密钥大小与秘密大小之比的下界，以及后一个问题中与Riis提出的开放问题相关的十个顶点图的上界。