---
title: "Gentzen-Type Formel System Representing Properties of Function and its Implementation"
authors:
  - "T. Nishimura"
  - "M. Nakanishi"
  - "M. Nogeta"
  - "Y. Iwamaru"
doi: ""
url: "https://ijcai.org/proceedings/1975/10"
pdf: "https://ijcai.org/proceedings/1975/0010.pdf"
venue: "Proceedings of the Fourth International Joint Conference on Artificial Intelligence"
year: 1975
pages: "57-63"
track: "Mathematical and Theoretical Aspects of A.I"
keywords:
---

# Gentzen-Type Formel System Representing Properties of Function and its Implementation

T. Nishimura, M. Nakanishi, M. Nogeta, Y. Iwamaru

*Proceedings of the Fourth International Joint Conference on Artificial Intelligence*, pages 57-63.

## Abstract

e describe a theorem-prover (called TKP 1), which is based on a Gentzen-type formal system (14). TKP 1 can directly deal with functionals and the composition of functionals, it comprises the fixed point operator and a kind of facility for induction. Let us attempt to prove P(F(x, y)) for F(x, y) such that F(x, y) =.Yo f" (x, y). Provided that P(F(x, y)) can be obtained from P ( f" (x, y)) n=O, 1, 2, ... , TKP 1 automatically gives the induction hypothesis P ( f" (x, y)), and then prove P(f"~ 1 (x, y)) . It can efficiently make proving procedure for properties of recursive programs. We can supply assumptions and definitions at will. TKP 1 displays an easily read proof-figure.