Automated deduction systems such as NuPrl and Mizar have facilities for accumulating results in libraries for later reference. There has also been some work in machine learning on identifying generalizations of previous proofs [Melis and Schairer 98] [Kolbe and Walther 94] [Mitchell, Keller et al. 86].

Publication and citation is essentially an instance of common subexpression elimination. In this talk I wish to study this interaction from a proof-theoretic perspective. I will describe a simple complete proof system for universal Horn equational logic with two new proof rules "publish" and "cite". These rules allow the inclusion of proved theorems in a library and later citation with specialization by a given substitution. The combinator corresponding to publish wraps the extract term to prevent beta-reduction upon citation. This essentially amounts to common subexpression elimination on proof terms. An interesting proof rule is the weakening rule that "forgets" something in the library. The corresponding combinator unwraps the extract term, allowing beta reduction to take place, which replaces all citations with the original proof.