BCK-formulas having unique proofs

Sachio Hirokawa

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    3 Citations (Scopus)


    The set of relevantly balanced formulas is introduced in implicational fragment of BCK-logic. It is shown that any relevantly balanced formula has unique normal form proof. Such formulas are defined by the ‘relevance relation’ between type variables in a formula. The set of balanced formulas (or equivalently one-two-formulas) is included in the relevantly balanced formulas. The uniqueness of normal form proofs is known for balanced formulas as the coherence theorem. Thus the result extends the theorem with respect to implicational formulas. The set of relevantly balanced formulas is characterized as the set of irrelevant substitution instances of principal type-schemes of BCK-λ-terms.

    Original languageEnglish
    Title of host publicationCategory Theory and Computer Science, Proceedings
    EditorsDavid H. Pitt, Pierre-Louis Curien, Samson Abramsky, Axel Poigne, David E. Rydeheard, Andrew M. Pitts
    PublisherSpringer Verlag
    Number of pages15
    ISBN (Print)9783540544951
    Publication statusPublished - 1991
    Event4th Biennial Summer Conference on Category Theory and Computer Science, 1991 - Paris, France
    Duration: Sep 3 1991Sep 6 1991

    Publication series

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


    Other4th Biennial Summer Conference on Category Theory and Computer Science, 1991

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)

    Fingerprint Dive into the research topics of 'BCK-formulas having unique proofs'. Together they form a unique fingerprint.

    Cite this