Writing programs that construct proofs (Q1820596): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Set OpenAlex properties.
 
(4 intermediate revisions by 3 users not shown)
Property / author
 
Property / author: Robert L. Constable / rank
Normal rank
 
Property / author
 
Property / author: Robert L. Constable / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: LCF / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/bf00244273 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2019651724 / rank
 
Normal rank

Latest revision as of 09:30, 30 July 2024

scientific article
Language Label Description Also known as
English
Writing programs that construct proofs
scientific article

    Statements

    Writing programs that construct proofs (English)
    0 references
    0 references
    0 references
    0 references
    1985
    0 references
    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.
    0 references
    Automath
    0 references
    automated reasoning
    0 references
    decision procedures
    0 references
    formal mathematics
    0 references
    intelligent systems
    0 references
    proof checking
    0 references
    LCF
    0 references

    Identifiers