Proving linear inequalities and identities of Shannon's information measures, possibly with linear constraints on the information measures, is an important problem in information theory. For this purpose, ITIP and other variant algorithms have been developed and implemented, which are all based on solving a linear program (LP). In particular, an identity $f = 0$ is verified by solving two LPs, one for $f \ge 0$ and one for $f \le 0$. In this paper, we develop a set of algorithms that can be implemented by symbolic computation. Based on these algorithms, procedures for verifying linear information inequalities and identities are devised. Compared with LP-based algorithms, our procedures can produce analytical proofs that are both human-verifiable and free of numerical errors. Our procedures are also more efficient computationally. For constrained inequalities, by taking advantage of the algebraic structure of the problem, the size of the LP that needs to be solved can be significantly reduced. For identities, instead of solving two LPs, the identity can be verified directly with very little computation.

翻译：证明香农信息措施的线性不平等和特征,可能对信息措施有线性限制,这是信息理论中的一个重要问题。为此目的,已经制定和实施了ITIP和其他变式算法,这些算法都基于解决线性程序(LP ) 。特别是,一个身份=0美元,通过解决两个LP来核实,一个为美元/日元/日元/日元,另一个为美元/日元/日元/日元/日元/日元/日元/日元。在本文件中,我们开发了一套可以通过象征性计算执行的算法。根据这些算法,制定了核实线性信息不平等和身份的程序。与基于LP 的算法相比,我们的程序可以产生分析证据,既可以人核查,也可以没有数字错误。我们的程序也是更有效率的计算。由于利用问题的代数结构,需要解决的LP的规模可以大大缩小。对于身份,而不是解决两个LP,可以直接用很少的计算来验证身份。