@inproceedings{3c1dc5e4f1a0496da1115c3b5f88c93f,
title = "BCK-formulas having unique proofs",
abstract = "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 {\textquoteleft}relevance relation{\textquoteright} 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.",
author = "Sachio Hirokawa",
note = "Funding Information: The author would like to thank to Y. Akama, R. Kashima, Y.Komori, H.Ono and M. Takahashi for their discussion on the subject. This work was partially supported by a Grant-in-Aid for Encouragement of Young Scientists No.02740115 of the Ministry of Education. Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1991.; 4th Biennial Summer Conference on Category Theory and Computer Science, 1991 ; Conference date: 03-09-1991 Through 06-09-1991",
year = "1991",
doi = "10.1007/BFb0013460",
language = "English",
isbn = "9783540544951",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "106--120",
editor = "Pitt, {David H.} and Pierre-Louis Curien and Samson Abramsky and Axel Poigne and Rydeheard, {David E.} and Pitts, {Andrew M.}",
booktitle = "Category Theory and Computer Science, Proceedings",
address = "Germany",
}