|
eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/5685
| Title: | Publication/Citation: A Proof-Theoretic Approach to Mathematical
Knowledge Management |
| Authors: | Kozen, Dexter
Ramanarayanan, Ganesh |
| Keywords: | computer science
technical report |
| Issue Date: | 16-Mar-2005 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-1985 |
| Abstract: | There are many real-life examples of formal systems that support
constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the future. In this paper we examine the operations of publication (remembering a proof) and citation (recalling a proof for reuse), regarding them as forms of common subexpression elimination on proof terms. We then develop this idea from a proof theoretic perspective, describing a simple complete proof system for universal Horn equational logic using three new proof rules, publish, cite, and forget. These rules can provide a proof-theoretic infrastructure for proof reuse in any system. |
| URI: | http://hdl.handle.net/1813/5685 |
| Appears in Collections: | Computing and Information Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
