@article{oai:metro-cit.repo.nii.ac.jp:00000138,
 author = {中西, 泰雄 and nakanishi, Yasuo},
 journal = {東京都立産業技術高等専門学校研究紀要, Research reports of Tokyo Metropolitan College of Industrial Technology},
 month = {Mar},
 note = {P(論文), In a proof by reducio ad absurdum (RAA),once we put false assumptions, it is hard to distiguish true statements from others in the following part of the proof. On the other hand, all intermediate statements in a direct proof are true. This means that a direct proof has far more informations than the corresponding RAA proof. Therefore, from educational point of view, it is very fruitful to write proofs without RAA.In our former research, we introduced an efficient logical system called WNK which is free from RAA. However, ordinary proofs used in mathematics are closer to NK of Gentzen rather than WNK. In this paper, we introduce another logical system PNK which is also free from RAA, and explain the planning method of PNK proofs by means of sequents.},
 pages = {70--76},
 title = {背理法を用いない論理体系とその証明計画},
 volume = {6},
 year = {2012},
 yomi = {ナカニシ, ヤスオ}
}