  A class of information inequalities, called Shannon-type inequalities (STIs),
can be proven via a computer software called ITIP. In previous work, we have
shown how this technique can be utilized to Fourier-Motzkin elimination
algorithm for Information Theoretic Inequalities. Here, we provide an algorithm
for extracting \emph{analytic} proofs of information inequalities. Shannon-type
inequalities are proven by solving an optimization problem. We will show how to
extract a \emph{formal} proof of numerically solved information inequality.
Such proof may become useful when an inequality is implied by several
constraints due to the PMF, and the proof is not apparent easily. More
complicated are cases where an inequality holds due to both constraints from
the PMF and due to other constraints that arise from the statistical model.
Such cases include information theoretic capacity regions, rate-distortion
functions and lossless compression rates. We begin with formal definition of
Shannon-type information inequalities. We then review the optimal solution of
the optimization problem and how to extract a proof that is readable to the
user.
