The higher-order-logic Formath (Q935562)

From MaRDI portal





scientific article
Language Label Description Also known as
English
The higher-order-logic Formath
scientific article

    Statements

    The higher-order-logic Formath (English)
    0 references
    0 references
    11 August 2008
    0 references
    This paper describes in detail the logic Formath, inspired by two HOL derivatives: HOL-4 and HOL-Light. Formath is designed from the point of view of a mathematician. This results in the introduction of a syntactical distinction between bound and free variables, the use of ``de Bruijn'' indices and extending the consequences to more than one consequence. The author proves the soundness of his system and ends with an interesting comparison of Formath and the classical HOL-4 and HOL-Light variants. The logical strength of Formath seems to be the same as the more established versions, but the axiomatization is rather elegant and has several novel features (for this context), e.g., multiple-conclusion sequents and a syntactic distinction between free and bound variables using an approach similar to ``de Bruijn'' indices.
    0 references
    higher-order logic
    0 references
    automated theorem proving
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references