Balanced formulas, BCK-minimal formulas and their proofs

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

3 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationLogical Foundations of Computer Science — Tver 1992 - 2nd International Symposium, Proceedings
EditorsAnil Nerode, Mikhail Taitslin
PublisherSpringer Verlag
Pages198-208
Number of pages11
ISBN (Print)9783540557074
DOIs
Publication statusPublished - Jan 1 1992
Event2nd International Symposia on Logical Foundations of Computer Science, Tver 1992 - Tver, Russian Federation
Duration: Jul 20 1992Jul 24 1992

Publication series

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

Other

Other2nd International Symposia on Logical Foundations of Computer Science, Tver 1992
CountryRussian Federation
CityTver
Period7/20/927/24/92

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hirokawa, S. (1992). Balanced formulas, BCK-minimal formulas and their proofs. In A. Nerode, & M. Taitslin (Eds.), Logical Foundations of Computer Science — Tver 1992 - 2nd International Symposium, Proceedings (pp. 198-208). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 620 LNCS). Springer Verlag. https://doi.org/10.1007/BFb0023874