@inproceedings{c2a2160fdd4b4c97924308c40829c498,

title = "Balanced formulas, BCK-minimal formulas and their proofs",

abstract = "The structure of normal form proof figures are investigated for implicatonal formulas in BCK-logic, in which each assumption can be used at most once. Proof figures are identified with λ-terms. A formula is balanced iff no type variable occurs more than twice in it. It is known that proof figure in βη-normal is unique for balanced formulas. In this paper, it is shown that closed λ-terms in β-normal form having balanced types are BCK-λ-terms in which each variable occurs at most once. A formula is BCK-minimal iff it is BCK-provable and it is not a non-trivial substitution instance of other BCK-provable formula. It is also shown that the set BCK-minimal formulas is identical to the set of principal type-schemes of BCK-λ-terms in βη-normal form.",

author = "Sachio Hirokawa",

year = "1992",

month = jan,

day = "1",

doi = "10.1007/BFb0023874",

language = "English",

isbn = "9783540557074",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "198--208",

editor = "Anil Nerode and Mikhail Taitslin",

booktitle = "Logical Foundations of Computer Science — Tver 1992 - 2nd International Symposium, Proceedings",

address = "Germany",

note = "2nd International Symposia on Logical Foundations of Computer Science, Tver 1992 ; Conference date: 20-07-1992 Through 24-07-1992",

}