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
PDF (1.7 MB)
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, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-416.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-416}, number = {UCAM-CL-TR-416} }