@phdthesis{oai:soar-ir.repo.nii.ac.jp:00018039,
 author = {中正, 和久},
 month = {Mar},
 note = {Thesis, 中正　和久. Mizar による群の直和分解の形式化. 信州大学, 2015, 博士論文. 博士（工学）, 甲第654号, 平成28年03月20日授与.},
 school = {信州大学(Shinshu university)},
 title = {Mizar による群の直和分解の形式化},
 year = {2016}
}