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未解决问题相关的十顶点图之一改进了上限。