Automated Hyper-Liking in An Electronic Mathematical Proof-Check Journal,
Abstract
The main objective of the grant is to establish a hyper-linked electronic proof-check journal. The name of the journal is Journal of Formalized Mathematics (JFM). It is available at http://mizar.uw.bialystok.pl/JFM. JFM consists of articles written originally in Mizar and translated mechanically into English. The original articles written in Mizar are in a machine readable form (and they are mechanically processed at the semantic level). This facilitates automatic insertion of hyper-links according to a uniform procedure. Automatic hyper-linking is fast: inserting more than 200 thousands hyper-links took about one hour, most of the time used for communication with the data base. The presented documentation consists of (1) typical articles submitted to JFM describing the formalization of fragments of the compendium, and (2) the annual report of the form requested by CS Dept. of ONR.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1996
- Accession Number
- ADA322951
Entities
People
- Andrzej Trybulec