@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",
note = "Funding Information: *Supportedb y a Grant-in-Aidf or Encouragemenotf Young ScientistsNo.0274011a5nd No.0375029o8f theM inistryo f Education Publisher Copyright: {\textcopyright} 1992, Springer Verlag. All rights reserved.; 2nd International Symposia on Logical Foundations of Computer Science, Tver 1992 ; Conference date: 20-07-1992 Through 24-07-1992",
year = "1992",
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",
}