Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management
Loading...
No Access Until
Permanent Link(s)
Other Titles
Author(s)
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.
Journal / Series
Volume & Issue
Description
Sponsorship
Date Issued
2005-03-16
Publisher
Cornell University
Keywords
computer science; technical report
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
References
Link(s) to Reference(s)
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-1985
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
Rights URI
Types
technical report