PROOF LOGS

PDF

Authors
  1. Kromodimoeljo, S.
  2. Pase, B.
Corporate Authors
ORA Canada, Ottawa ONT (CAN);Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
Abstract
The report describes proof logs in NEVER as they appear in EVES, version 2.4.2. The description of proof logs in this report is informal. Presented are: the background to the proof logging effort, including the objectives of the effort from proof checking and proof browsing perspectives; the notion of a proof as a sequence of equivalence preserving transformations on a formula; the basic framework for proof logs; a description of the inference rules, grouped in sections according to their classification. Finally, an assessment of the work with respect to the objectives.
Keywords
Computer program documentation;Trace logic;Computer logging routines;Computer logs
Report Number
TR-95-5471-03 — Technical Report
Date of publication
01 Jun 1995
Number of Pages
47
DSTKIM No
96-02606
CANDIS No
497166
Format(s):
Document Image stored on Optical Disk;Hardcopy

Permanent link

Document 1 of 1

Date modified: