Show simple item record

dc.contributor.authorAllen, Stuart F.en_US
dc.contributor.authorConstable, Robert L.en_US
dc.date.accessioned2007-04-04T20:21:17Z
dc.date.available2007-04-04T20:21:17Z
dc.date.issued2006-01-27en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2014en_US
dc.identifier.urihttps://hdl.handle.net/1813/5714
dc.description.abstractMathematical and program-code text is unique because significant portions of it can be anchored to counterparts in formal logical theories that are implemented by computer systems. These systems check formal proofs for correctness and trace logical dependencies among assertions. When elements of expository text, such as definitions and theorems, are formally linked to their implemented counterparts, we call the texts semantically anchored. Such texts exhibit considerable depth and authority. It is possible to leverage substantial investments made by governments, research laboratories, corporations, and universities in creating large collections of computerchecked and interactively-generated formal mathematics, making this research investment, these collections, accessible to an extended community of authors, researchers, students and teachers involved with mathematics. We advocate extending common authoring tools (text editors as opposed to formal proof development tools) so that they can easily produce semantically anchored documents suitable for dissemination along with the formal mathematics to which they are anchored; some texts would be newly authored, while others would be static textbased resources improved by anchoring. These tools will enable authors to create these documents by drawing on a large already existing and growing collection of formal material. We expect that anchored documents will enable interconnected collections where the computers support exact common reference among concepts and thus greatly facilitate collaborative contributions to online collections and provide large-scale coherency among mathematical texts.en_US
dc.format.extent209336 bytes
dc.format.extent209336 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/pdf
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleEnabling Large Scale Coherency Among Mathematical Textsen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics