Higher-order computational logic

John W. Lloyd*

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

    4 Citations (Scopus)

    Abstract

    This paper presents a case for the use of higher-order logic as a foundation for computational logic. A suitable polymorphically-typed, higher-order logic is introduced and its syntax and proof theory briefly described. In addition, a metric space of closed terms suitable for knowledge representation purposes is presented. The approach to representing individuals is illustrated with some examples, as is the technique of programming with abstractions. The paper concludes by placing the results in the wider context of previous and current research in the use of higherorder logic in computational logic.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    PublisherSpringer Verlag
    Pages105-137
    Number of pages33
    ISBN (Print)3540439595, 9783540439592
    DOIs
    Publication statusPublished - 2002

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume2407
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Fingerprint

    Dive into the research topics of 'Higher-order computational logic'. Together they form a unique fingerprint.

    Cite this