Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Publication/Citation: A Proof-Theoretic Approach to Mathematical
    Knowledge Management

Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management

File(s)
TR2005-1985.pdf (146.69 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5685
Collections
Computing and Information Science Technical Reports
Author
Kozen, Dexter
Ramanarayanan, Ganesh
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.

Date Issued
2005-03-16
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-1985
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance