@article{oai:metro-cit.repo.nii.ac.jp:00000145,
 author = {中西, 泰雄 and nakanishi, Yasuo},
 journal = {東京都立産業技術高等専門学校研究紀要, Research reports of Tokyo Metropolitan College of Industrial Technology},
 month = {Mar},
 note = {P(論文), In a heuristic process of proof in mathematics, we try not only forward derivationsfrom the assumptions such as `from A, we get B' but also backward derivations from theconclusion such as `in order to get C, we need D'. Thus, we have to discover all the statementswhich connect assumptions with the conclusion, to complete the planning of the proof. Wedefine `heuristic tableau' as a tableau which consists of those statements aranged in the order of discovery with symbols which express the logical relations of those statements. We suggesta planning method of proofs by using heuristic tableaus. For a concrete explanation, we use the first order NK system of Gentzen to explain our method. Our method gives an algorithmto prove arbitrary tautologies of the first order NK system, and is also valid for practical mathematics which is not necessarily formalized in symbolic logic.},
 pages = {26--40},
 title = {発見タブローによる証明計画},
 volume = {7},
 year = {2013},
 yomi = {ナカニシ, ヤスオ}
}