KnowledgeBase » 
SEMINAR
» ID = 567
A Proof-Theoretic Approach to Knowledge Acquisition"
by Dexter Kozen
2001-2002
There are many examples in real life of formal systems that support certain constructions or proofs, but that do not provide direct support for remembering what was done so that it can be recalled in the future. This task is usually left to some metasystem that is typically provided as an afterthought. For example, programming language design usually focuses on the programming language itself; the mechanism for accumulating useful code in libraries is more of a systems issue and is considered a separate design task. Mathematics deals with the construction of proofs, but not on their publication; that is the domain of the journal publishers.
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.