Practical logic (Invited presentation)

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

    Abstract

    This talk is about getting correct programs by plagiarizing proofs that others have already produced. The method provides an alternative to verification as practised to the south of here in Brisbane. In ancient times in the East mathematicians worked out their mathematics to solve (practical) problems. In the West they concentrated on abstract proofs with calculations almost as an afterthought. At the beginning of this century the Intuitionist mathematicians refused to accept any mathematics which did not give a construction of the object which was being proved to exist. The present day industry of extracting programs from proofs started by using this logic. (Incidentally the logic was formulated in a way that was anathema to the Intuitionists themselves.) There is a general approach which most people seem to follow. Unfortunately we have no algorithm to implement this approach. However we shall show how to apply the general approach in several different contexts including Buss’s logic which gives exactly programs for polynomial-time computable functions and Linear Logic which allows the measurement of resources consumed. All of this depends on actually having proofs—and worse than that—proofs in the formal system. We shall also present a framework for getting over this difficulty and using real proofs—the sort you find in books. This last part has not yet been implemented but we hope by the time of the talk that the others will have been.

    Original languageEnglish
    Title of host publicationAlgorithms and Computations - 6th International Symposium, ISAAC 1995, Proceedings
    PublisherSpringer
    Number of pages1
    ISBN (Print)3540605738, 9783540605737
    Publication statusPublished - 1 Jan 1995
    Event6th International Symposium on Algorithms and Computations, ISAAC 1995 - Cairns, Australia
    Duration: 4 Dec 19956 Dec 1995

    Publication series

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

    Conference

    Conference6th International Symposium on Algorithms and Computations, ISAAC 1995
    CountryAustralia
    CityCairns
    Period4/12/956/12/95

    Cite this