---
title: "An Automatic Theorem Prover Generating a Proof in Natural Language"
authors:
  - "Masakazu Nakanlshi"
  - "Morio Nagata"
  - "Kenji Ueda"
doi: ""
url: "https://ijcai.org/proceedings/1979/139"
pdf: "https://ijcai.org/proceedings/1979/0139.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# An Automatic Theorem Prover Generating a Proof in Natural Language

Masakazu Nakanlshi, Morio Nagata, Kenji Ueda

*Proceedings of the Sixth International Joint Conference on Artificial Intelligence*.

## Abstract

An automatic theorem prover which displays a proof in system proves properti~s of recursive programs, and the proof. Then it translates the tree into the proof traverse. The proof written by this system is easy to instead of notations of logics, and some redundant and natural language is described. This constructs a proof tree corresponding to text in English by means of the tree read, because the English text is placed trivial statements are disappeared.