## 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 language | English |
---|---|

Title of host publication | Logical Foundations of Computer Science — Tver 1992 - 2nd International Symposium, Proceedings |

Editors | Anil Nerode, Mikhail Taitslin |

Publisher | Springer Verlag |

Pages | 198-208 |

Number of pages | 11 |

ISBN (Print) | 9783540557074 |

DOIs | |

Publication status | Published - 1992 |

Externally published | Yes |

Event | 2nd International Symposia on Logical Foundations of Computer Science, Tver 1992 - Tver, Russian Federation Duration: Jul 20 1992 → Jul 24 1992 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 620 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 2nd International Symposia on Logical Foundations of Computer Science, Tver 1992 |
---|---|

Country/Territory | Russian Federation |

City | Tver |

Period | 7/20/92 → 7/24/92 |

## All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)