@article{oai:metro-cit.repo.nii.ac.jp:00000121,
 author = {中西, 泰雄 and nakanishi, Yasuo},
 journal = {東京都立産業技術高等専門学校研究紀要, Research reports of Tokyo Metropolitan College of Industrial Technology},
 month = {Mar},
 note = {P(論文), Reducio ad absurdum (RAA) is a typical method of proving in mathematics. In aproof by RAA, however, once we put false assumptions, it is hard to distiguish true propositionsfrom other propositions in the following part of the proof. On the other hand, all intermediatepropositions in a direct proof are true and mathematically understandable. Therefore, fromeducational point of view, it is very fruitful to write proofs without RAA. By rewriting theproof by RAA into a direct one, moreover, we sometimes get more general theorem than theoriginal one. In this paper, we introduce a logical system (WNK) which is free from RAA.The proof diagrams of WNK allow plural conclusions as well as plural assumptions, whichmakes the proof diagrams simple. Moreover, we show that proofs of WNK can be plannedefficiently by using `sequents' like in Gentzen's LK.},
 pages = {88--98},
 title = {背理法を用いない効率的な証明のシーケントによる計画法},
 volume = {5},
 year = {2011},
 yomi = {ナカニシ, ヤスオ}
}