論理型言語PROLEG から双極議論フレームワークへの変換のCoqによる形式化と証明

中西 瑠海; 森口 草介; 高橋 和子

論文・著書情報

タイトル

和文:	論理型言語PROLEG から双極議論フレームワークへの変換のCoqによる形式化と証明
英文:

著者

和文:	中西瑠海, 森口草介, 高橋和子.
英文:	中西瑠海, Sosuke Moriguchi, 高橋和子.

言語

Japanese

掲載誌/書名

和文:	第81回全国大会講演論文集
英文:

巻, 号, ページ

Vol. 2019 No. 1 pp. 199-200

出版年月

2019年3月

出版者

和文:
英文:

会議名称

和文:
英文:

開催地

和文:
英文:

アブストラクト

論理型言語PROLEG から双極議論フレームワークへの変換の正当性について述べる．PROLEGは条文を論理プログラムとして記述することで, 計算による法的推論を行うためのシステムである．推論過程が明確になる一方で，PROLEG による記述では推論規則間の関係や推論の全体構造が把握しにくいことから，意味論を保持したまま，グラフ表現が可能な双極議論フレームワークに変換する手法が提案されている．本稿ではPROLEG から双極議論フレームワークへの変換を証明器支援系Coq を用いてモデル化し，変換後の双極議論フレームワークがもとのPROLEG プログラムの意味論を保持していることを形式的に証明する．

【重要】T2R2・STARSearchの停止と後継システムについて

論文・著書情報