2011年6月2日，應(yīng)太陽集團tyc5997邀請，來自日本大學(xué)計算邏輯研究所的小林英恒教授為我院師生做了題目為“基于定理證明工具Isabelle/HOL的自動推理系統(tǒng)”的學(xué)術(shù)報告，劉曉平院長主持報告會。小林教授首先對Isabelle/HOL這一著名的定理證明工具進行了介紹。隨后就為什么要設(shè)計自動推理系統(tǒng)進行解釋，并例舉出目前世界著名的一些自動推理系統(tǒng)，最后小林教授就其自己提出的H-prover系統(tǒng)進行了詳細的說明，并演示了相關(guān)工作。
在場師生以熱烈的掌聲感謝小林教授精彩的報告，并積極向小林教授請教，小林教授對我院師生的工作給予指導(dǎo)，報告會在熱烈的掌聲中結(jié)束。報告會之后，在學(xué)院有關(guān)同志的陪同下，小林教授還參觀了安全關(guān)鍵工業(yè)測控技術(shù)教育部工程研究中心，饒有興趣地與相關(guān)老師進行了交流和溝通。
小林英恒教授，畢業(yè)于日本京都大學(xué)，主修數(shù)學(xué)，目前就職于日本大學(xué)科學(xué)與技術(shù)學(xué)院數(shù)學(xué)系，同時也是中國科學(xué)研究院高級研究員。
TOP
