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

footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会