Writing programs that construct proofs
type: Item
instance of: scholarly article
title: Writing programs that construct proofs
zbMATH Open document ID: 0615.68063
DOI: 10.1007/BF00244273
author: T. B. Knoblock
author: J. L. Bates
author: Robert Constable
published in: Journal of Automated Reasoning
publication date: 1985-01-01T00:00:00Z
review text: When we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and into computer systems used to build such theories. We illustrate the methods as they were applied in the \(\lambda\)-PRL system, essentially using the ML programming language from Edinburgh LCF as the formalized metalanguage. We report our experience with such an approach emphasizing the ideas that go beyond the LCF work, such as transformation tactics and special purpose reasoners. We also show how the validity of tactics can be guaranteed. The introduction places the work in historical context and the conclusion briefly describes plans to carry the methods further. The majority of the paper presents the \(\lambda\)-PRL approach in detail.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3997192
zbMATH Keywords: Automath
zbMATH Keywords: automated reasoning
zbMATH Keywords: decision procedures
zbMATH Keywords: formal mathematics
zbMATH Keywords: intelligent systems
zbMATH Keywords: proof checking
zbMATH Keywords: LCF
describes a project that uses: LCF
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244273
OpenAlex ID: W2019651724
description: scientific article; zbMATH DE number 3997192