Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management
| dc.contributor.author | Kozen, Dexter | en_US |
| dc.contributor.author | Ramanarayanan, Ganesh | en_US |
| dc.date.accessioned | 2007-04-04T19:42:41Z | |
| dc.date.available | 2007-04-04T19:42:41Z | |
| dc.date.issued | 2005-03-16 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 150208 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-1985 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/5685 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management | en_US |
| dc.type | technical report | en_US |
Files
Original bundle
1 - 1 of 1