Department of Computer Science and Technology

Technical reports

DECLARE: a prototype declarative proof system for higher order logic

Donald Syme

February 1997, 25 pages

DOI: 10.48456/tr-416

Abstract

This report describes DECLARE, a prototype implementation of a declarative proof system for simple higher order logic. The purpose of DECLARE is to explore mechanisms of specification and proof that may be incorporated into other theorem provers. It has been developed to aid with reasoning about operational descriptions of systems and languages. Proofs in DECLARE are expressed as proof outlines, in a language that approximates written mathematics. The proof language includes specialised constructs for (co-)inductive types and relations. The system includes an abstract/article mechanism that provides a way of isolating the process of formalisation from what results, and simultaneously allow the efficient separate processing of work units. After describing the system we discuss our approach on two subsidiary issues: automation and the interactive environment provided to the user.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-416,
  author =	 {Syme, Donald},
  title = 	 {{DECLARE: a prototype declarative proof system for higher
         	   order logic}},
  year = 	 1997,
  month = 	 feb,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-416},
  number = 	 {UCAM-CL-TR-416}
}