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

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

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

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

Download BibTeX Cite

Proceedings of the Fourth International Joint Conference on Artificial Intelligence. Mathematical and Theoretical Aspects of A.I. 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.

T. Nishimura, M. Nakanishi, M. Nogeta, and Y. Iwamaru. 1975. Gentzen-Type Formel System Representing Properties of Function and its Implementation. In Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75. IJCAI, 57–63. https://ijcai.org/proceedings/1975/10

@inproceedings{ijcai1975p10,
  title     = {Gentzen-Type Formel System Representing Properties of Function and its Implementation},
  author    = {Nishimura, T. and Nakanishi, M. and Nogeta, M. and Iwamaru, Y.},
  booktitle = {Proceedings of the Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-75}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Patrick Winston and Carl Hewitt},
  pages     = {57--63},
  year      = {1975},
  note      = {Mathematical and Theoretical Aspects of A.I},
  url       = {https://ijcai.org/proceedings/1975/10},
}

TY  - CPAPER
TI  - Gentzen-Type Formel System Representing Properties of Function and its Implementation
AU  - Nishimura, T.
AU  - Nakanishi, M.
AU  - Nogeta, M.
AU  - Iwamaru, Y.
T2  - Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1975
SP  - 57
EP  - 63
UR  - https://ijcai.org/proceedings/1975/10
ER  -