日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

論理型言語 PROLEG に対応する双極議論フレームワー
クの意味論について
川崎 樹

森口 草介

高橋 和子

論理型プログラム PROLEG から双極議論フレームワークへの変換について述べる．PROLEG は日本における法律要件を記述するために開発されたシステムであり，民法や刑法を記述するには適しているが，それを実際の案件に適用したときにおこる推論過程や論証のやりとりなどは簡単にはわからない．これらを明確に表現するために PROLEG
プログラムを，論証および論証間の攻撃関係，支持関係によって議論を表現するシステムである双極議論フレームワークに変換する．本稿では，非循環な PROLEG プログラムを対象として，変換によって得られる双極議論フレームワークに意味論を与え，この変換が解集合で与えられた PROLEG の意味論を保持することを示す．また，循環を含む場合についてのこの手法の拡張について議論する．

成要件，(要件) 事実という．また，法には違法性を否

1 はじめに定する阻却事由など例外的なルールがあることもあ

ここ 30 年ほど計算機上の議論学 (argumentation) にる．法が効果を発揮するための前提条件の一つに例外関する研究は非常にさかんに行われている [4]．議論的なルールが成立しないことがあげられる．PROLEG学の考え方を使うことで，論理的なモデルが提示でではこの構成要件，事実，例外的なルールの関係を論き，結論だけでなく，結論を出すまでの経過や各論証理プログラムで表現する．の因果関係についても明確に示すことができるため，PROLEG の記述言語は Prolog を拡張したもので，マルチエージェント環境での合意形成，対話システ

その記述は 2 種類の節からなる．一つは一般的な規ム，非単調推論といった人工知能の分野だけでなく，則であり，もう一つは例外と呼ばれる特殊な規則であ

システム設計における信頼性検証などソフトウェア工る．例えば，殺人罪を PROLEG で記述することを考学の分野でも議論学が応用されている．法的推論も議える．殺人罪の構成要件として「自然人である」，「殺論学の有用な応用の一つとして期待されている分野

人行為がある」「殺意がある」の三つがあるとして，である．

「自然人であり，殺人行為があり，殺意があったなら裁判におけるやりとりは一種の議論と考えられるば殺人罪が成り立つ」ことを PROLEG で記述するとが，判決を出す過程は人間が行っており，システム化次のように書くことができる．

されていないのが現状である．法律とその適用をシス

殺人罪 <= 自然人, 殺人行為, 殺意.

テム化し計算によって法的推論を行うために PROLEG

また，殺人罪に対する例外として正当防衛を考えるシステムが開発された [5]．と，「正当防衛ならば殺人罪でない」ことは PROLEG

法には効果を発揮するための前提条件があり，前提で以下のように記述できる．

条件を満たすための事実が必要である．それぞれを構

exception(殺人罪, 正当防衛).
この 2 節から推論を行う．例えば三つの構成要件にOn the semantics of the Bipolar Argumentation Framework
corresponding to logical language PROLEG.
Tatsuki Kawasaki, Sosuke Moriguchi, Kazuko Takahashi, 関西学院大学, Kwansei Gakuin University.

ついて全ての事実が確認できれば，殺人罪が成立する．一つでも事実が確認できなければ殺人罪は成立しない．また，正当防衛が成立するなら，たとえ殺人罪の構成要件の全て事実が確認できていても殺人罪は成立しない．このように推論を行い結論を導く．

したまま変換することを可能にした．
本稿の構成は以下の通りである．まず，2 節で PRO-

訴訟現場において，ある法の適用もしくは不適用のLEG について述べる．次に，3 節で我々が対象とすプロセスを提示することは重要である．法曹は結果とる BAF を定義し，それに意味論を与える．その後，4

理由は提示するが，構成要件や事実を用いて推論過程

節で PROLEG プログラムから BAF への変換手法をを示すことはない．そのため原告と被告の双方が判決述べる．5 節では刑法を記述した PROLEG プログラに十全に納得しない可能性が考えられる．そのため，ムが非循環であることを利用し，変換して得られた構成要件や事実の関わりを踏まえた推論過程を示す

BAF が PROLEG プログラムの意味を保持しているこ必要がある．その際，PROLEG の記述を提示しても，とを証明する．6 節で循環を含むプログラムの意味論

論理プログラムは法曹にはなじみのない記述法式でについて議論し，7 節で結論と今後の課題について述ある上に推論過程が明示されていないので，理解は容べる．

易ではない．
そこで，法的推論を一種の議論とみなせることを利2 論理型言語 PROLEG用する．議論の過程や結論に至る理由を明確にする研論理型言語 PROLEG は Prolog を拡張して開発され究として，議論システムに基づく手法が多く提案された裁判支援を目的とする記述言語である [5]．ある法ている [4]．Dung は抽象レベルで議論の仕組みをとらに対して，構成要件，事実，例外的なルールを組み合えた議論フレームワーク (Argumentation Framework,わせ記述することで，その法の真偽を判定する．構成AF) を提唱した [3]．この枠組みでは論証および論証

要件は法が効果を発揮するための条件であり，事実も間における攻撃関係の二項組で定義され，どの論証がしくは他の法の成立が必要となる．例外的なルールと受理されたかを計算することで意味論が与えられては法もしくは構成要件の成立を，例外的に否定する効いる．その後この手法から多くの派生的研究が行われ果を持つ．例外的なルールが認められれば，他の要素ている．

によって成立していても例外が認められ不成立とな

双 極 議 論 フ レ ー ム ワ ー ク (Bipolar Argumentationる．佐藤らは，PROLEG を用いて記述されたプログ

Framework, BAF) もその一つであり，Dung の議論フラムを以下のように定義している．法と構成要件の関

レームワークに攻撃関係だけではなく支持関係を追係を規則で表し，例外的なルールを例外で表した．

加した 3 項組で定義されている [1]．裁判においては攻撃あるいは支持となる論証が陽に現れるため，AFよりも BAF による表現が望ましい．
本研究の目標は，計算機システムや論理プログラミ

ここで，H, B, B1 , . . . , Bn はアトムである．
定義 1. PROLEG プログラム P は，P = ⟨R, E⟩ の 2 つ組で定義される．R は規則の有限集合，E は例外の有限集合である．

ングになじみのない法曹に対して裁判における推論

定義 2. P 中において，H ⇐ B1 , . . . , Bn の形式で記述過程や議論の進行状況を明確にすることであり，このされた節を規則という．特に，H ⇐ の形式で記述さ目標を達成するために，PROLEG の記述を BAF に変れた規則を事実という．

換するアプローチをとる．また，BAF における支持

定義 3. P 中において，exception(H, B) の形式で記述関係を論証間におけるものではなく，論証の集合と論された節を例外という．

証の間におけるものに拡張し，それに意味論を与え以下に例を示す．
．

る．BAF については Cayrol らが意味論を与えているが [2]，PROLEG に対応する BAF については既存の意味論を適用してもそのままでは両者の意味論は一致しない．本研究では BAF に新たに意味論を与えることで PROLEG プログラムから BAF へ意味を保存

例 1.

p <= q1 ,q2.
exception (q1 ,r).
q2 <=.
r <=.

p <= q1,q2 は 規 則 で あ る ．p <= q1,q2 で は ，限集合であり，ATT ，SUP はそれぞれ ATT ⊆ AR × AR，q1，q2 が 真 で あ る な ら ば p は 真 と な る こ と を 表SUP ⊆ (2AR \ ∅) × AR で 定 義 さ れ る 集 合 で あ る ．

す．q2<=，r<=は事実であり，真であることを表す．

(B, A) ∈ ATT を att(B, A)，(A, A) ∈ SUP を sup(A, A)

exception(q1,r) は例外である．r が真であるならと記述する．

ば，その時に限り q1 は必ず偽となることを表す．

定義 9. ある論証 A ∈ AR に対して，A の関連集合 relA

以下では，P を可能な置換によって基礎化されたもを relA = {B | att(B, A)} ∪ {B | B ∈ A ∧ sup(A, A)} で定義のとして扱う．

する．

定 義 4. 関 数 head，body を 以 下 の よ う に 定 義

定義 10. 高さ関数 h を，baf = ⟨AR, ATT, SUP⟩ の AR

す る ．規 則 R = H⇐ B1 , . . . , Bn に つ い て ，から非負整数への関数として以下のように定義する．

head(R) = H ，body(R) = {B1 , . . . , Bn } で あ る ．例(relA = ∅)0h(A) = maxB∈relA h(B) + 1 (otherwise)
ラベリングは BAF における各論証の受理性を表す．

外 E = exception(H, B) に つ い て ，head(E) = H ，body(E) = {B} である．
また，佐藤らは PROLEG プログラム P の解集合を以下のように定義した．

ラベリングにより各論証の受理性は異なるため，ラベ

定義 5. P に対して解集合 M を次のように定義すリングは BAF に意味を与えることに他ならない．こ= {H ⇐ B1 , . . . , Bn ∈ R | ∀E ∈こでは，PROLEG プログラムから BAF へ変換するたE, if head(E) = H then body(E) ⊈ M} の最小モデルでめ，PROLEG プログラムの意味を保持するためのラある．

ベリングを与える．以下のようにラベリングを定義

る ．M が 集 合 PM

本稿ではさらに各アトムに対して，関連集合を定義する．

する．さらに PROLEG プログラムに対してレベル関

定義 11. baf = ⟨AR, ATT, SUP⟩ に対して，ラベリン数を定義する．

グ L とは AR から {in, out} への関数である．また，定義 6. P 中の各アトム A に対して，関連集合 rP (A) を∪次のように定義する．rP (A) = R∈R∧head(R)=A body(R) ∪∪E∈E∧head(E)=A body(E)A ∈ (2AR \ ∅) に対して，∀A ∈ A, L(A) = in のときにL(A) = in，そうでなければ L(A) = out とする．

定義 7. レベル関数 lP を，P 中のアトムから非負整数定 義 12. baf = ⟨AR, ATT, SUP⟩ に お い て ，任 意 のへの関数として以下のように定義する．
(rP (A) = ∅)1lP (A) = maxB∈rP (A) lP (B) + 1 (otherwise)lP が一意に定まるとき，P を非循環であるという．

A ∈ AR に対するラベリング L が以下を満たすな

まず初めに非循環な PROLEG プログラムを対象にする．よって，lP (A) = n のとき，A のレベルは n である．

また，完全ラベリングを以下のように定義する．

らばそのラベリングを完全ラベリングという．

• (∀B ∈ AR, ¬att(B, A)) ∧ (∀A ⊆ AR, ¬sup(A, A)) であるならば L(A) = in．

• (∀B ∈ AR, att(B, A) ⇒ L(B) = out) ∧ (∃A ⊆AR, sup(A, A) ∧ L(A) = in) であるならば，L(A) =in．

3 双極議論フレームワーク• そうでなければ L(A) = out．

Cayrol らは，抽象議論フレームワークを拡張し，論任意の非循環な BAF には，唯一つの完全ラベリン

証と論証間の二項関係として，攻撃の支持の 2 種類をグが存在する．また，{A | L(A) = in} である集合を用いた 3 つ組で定義される双極議論フレームワーク

BAF の受理集合という．

(BAF) を提唱した [2]．本研究では支持関係を拡張し，

例 2. 次の BAF を考える．

論証と論証の集合の間の二項関係として定義する．

⟨{a, b, c, d}, {(b, a), (d, b)}, {({c}, a)}}⟩定 義 8. 双 極 議 論 フ レ ー ム ワ ー ク BAF は baf =この BAF の完全ラベリングを図 1 に示す．

⟨AR, ATT, SUP⟩ の組として定義される．AR は論証の有• ExistenceS upport={({ex(H)}, H) | H∈Existence}• Absence=Literal\({head(R) | R∈R} ∪{head(E) | E ∈ E})• AbsenceAttack = {(ab(B), B) | B ∈ Absence}• AR = Literal ∪ {ex(H) | H ∈ Existence} ∪{ab(B) | B ∈ Absence}• ATT = Exc ∪ AbsenceAttack• SUP = Rule ∪ ExistenceS upport
図1

完全ラベリング付き BAF

4 PROLEG プログラムから双極議論フレームワークへの変換
PROLEG プログラム P を BAF に，P の解集合とBAF の受理集合が一致するように変換する．この変換により P 中のアトム，規則，例外はそれぞれ論証，例 3. 次の PROLEG プログラムを考える．

p <= q1 ,q2.
exception (q1 ,r).
q2 <=.
r <=.
この PROLEG プログラムを変換して得られた BAFは次のようになる．
⟨{p, q1 , q2 , r, ex(q2 ), ex(r)}, {(r, q1 )},示的には現れない二つの論証を BAF に追加する．1{({q1 , q2 }, p), ({ex(q2 )}, q2 ), ({ex(r)}, r)}⟩
論証 q1 ，q2 は集合で p を支持している．またこのつは P 中のあるアトムに対して，そのアトムが成立す

例では q2 ，r に対してそれぞれ存在論証が作成されて支持関係，攻撃関係に変換される．さらに，P 中に明るか否かが，P 中に明記されていないことを示す不在論証である．P の記述の中で一度も頭部として現れないアトムは，成立するか否かが明記されておらず，解集合に含まれることはない．一方で，BAF では攻撃も支持もされていない論証のラベルは in である．この差を埋めるため，不在論証を加えそのアトムを攻撃する．あるアトム A に対する不在論証を ab(A) と書く．

いる．図 2 にこの BAF のラベリング付きグラフ表現を示す．

5 意味論を保持していることの証明
PROLEG プログラムを変換して得られた BAF はPROLEG プログラムの意味論を保持している．
定理 1. baf を PROLEG プログラム P を変換して得られた BAF とする．また，M を P の解集合とし，L をもう一つは，事実の存在を示す存在論証である．事

baf の完全ラベリングとする．このとき，P に出現す

実は体部にアトムを持っていないが，BAF では支持る任意のアトム H について，L = in ならばそのときは二項関係である．そのため存在論証を加えそのアトに限り H ∈ M である．

ムを支持する．事実として記述されたアトム A に対これの証明を示す．

して，存在論証を ex(A) と書く．

Proof. アトムのレベル n に関する帰納法による．baf

定 義 13. PROLEG プ ロ グ ラ ム ⟨R, E⟩ か ら ba f =において高さ 0 の論証は不在論証もしくは存在論証⟨AR, ATT, SUP⟩ への変換を以下のように定義する．
∪• Literal = R∈R ({head(R)} ∪ body(R))∪∪
E∈E ({head(E)} ∪ body(E))

であるから，明らかに P のレベルは baf における高さ• Rule = {(body(R), head(R)) | R ∈ R ∧ body(R) , ∅}れていないアトムである．もし H が事実であるなら• Exc = {(B, H) | exception(H, B) ∈ E}

ば，H ∈ M である．この時，事実は sup({ex(H)}, H) に

• Existence = {H | H ⇐∈ R}

変換されており (かつ他の論証からの攻撃関係はない)，として保持される．

n = 1 の時，H は事実もしくは一度も頭部として現図2

変換して得られた完全ラベリング付き BAF

L(ex(H)) = in であるから L(H) = in である．もし H

則 H ⇐ B1 , . . . , Bm . を変換して得られた関係であり，が一度も頭部として現れていないアトムであるなら，

B1 , . . . , Bm のレベルは n より小さいので，仮定よりexception(ab(H), B) に変換されており，L(ab(H)) = in

B1 , . . . , Bm ∈ M である． M は最小モデルであるので，であるから L(H) = out である．よって，L(H) = in でH ∈ M である．
従って，全てのレベル n について，L(H) = in でああるならそのときに限り H ∈ M である．

n ≥ 2 について，任意の k < n で定理を満たすと仮るならばそのときに限り H ∈ M である．

□′定する．つまり，レベル k の任意のアトム H について H ′ ∈ M であるなら L = in であるとする．H のレベルは 1 より大きいので H は規則または例外，あるいはその両方に出現している．
初めに H ∈ M の時 L(H) = in であることを示す．

M は最小モデルなので，全ての m について Bm ∈ Mであるような規則 H ⇐ B1 , . . . , Bm が存在し， B ∈ Mであるような例外 exception(H, B) が存在しない．bafにおいて規則は sup({B1 , . . . , Bm }, H) に変換される．

B1 , . . . , Bm のレベルは n より小さいので，仮定より，全ての m について L(Bm ) = in である．また例外はatt(B, H) に変換され，B < M であり， B のレベルは nより小さいので L(B) , in である．よって L(H) = in

6 循環を含むプログラムへの拡張についての考察
ここまでは，非循環な PROLEG プログラムのみを取り上げた．これは PROLEG が対象とする日本の法，特に刑法では適切に構成されているならば規則同士が衝突するようなことがないためである．しかし，PROLEG プログラムは，循環を含む記述も許す．たとえば [6] では以下のような例が記述されている．

exception (q1 ,q2).
exception (q2 ,q1).
q1 <=.
q2 <=.

である．
次に，L(H) = in であるならば H ∈ M であることを示す．H は他のいくつかの論証から支持または攻撃されている，あるいは支持も攻撃もされている．
よって L(H) = in であるならば，任意の H を攻撃している論証 B について L(B) , in である．この攻撃関係は例外 exception(H, B) を変換して得られた関係であり，仮定より B < M である．また，全ての m について L(Bm ) = in であるような H を支持している論証集合が存在している．このような支持関係は規q1 と q2 がそれぞれに対して例外を主張しており，一方を認めるともう一方が認められない記述となっている．この PROLEG プログラムの解集合は，{q1} および {q2} の二つである．
こ の プ ロ グ ラ ム を 4 節 の 手 法 に よって BAF に 変 換 す る と ，⟨{q1, q2, ex(q1), ex(q2)},{(q1, q2), (q2, q1)}, {({ex(q1)}, q1), ({ex(q2)}, q2)}⟩ と なる．この BAF における完全ラベリングは二つ考えられ，一方は q2 だけを out にするもの，もう一方はq1 だけを out にするものである．先ほど挙げた解集

合とこのラベリングはそれぞれ対応している．

る必要はないと考えている．

非循環な場合の証明はレベル関数および高さ関数を用いて行った．しかし循環が存在するとレベル関数お7 おわりによび高さ関数が定義できない．この問題は，プログラ

非循環な PROLEG プログラムから BAF への変換

ムや BAF に対する関数をどのような意味に対してもを行った．変換した BAF に対して，PROLEG プログ単一に定義しようとしたために発生する問題である．

ラムの解集合を保持する意味論を与え，さらに変換

そこで，解集合やラベリングに応じた関数を定義し，して得られた BAF が解集合を保持していることを証その上で非循環な場合に似た証明を行うことを考え明した．また，循環する PROLEG プログラムに対すている．証明の完成は今後の課題だが，成功すれば一る考察を行った．今後は厳密に PROLEG と対応する

般の標準論理プログラムを意味的に等価な BAF に変BAF の意味論を与え，証明を行う．

換する手法とその正当性を与えることができる．
ただし，もう一点，PROLEG 特有の意味論に関する問題が存在する．以下のプログラムを考える．

q1 <= q2.
q2 <= q1.
このプログラムは q1 と q2 が互いに導出し合う，ある種の循環論法になっている．PROLEG では解集合を最小モデルと規定しているため，このプログラムの解集合は空集合唯一つに定まる．一方，変換後のBAF では二つの完全ラベリングがあり，一つは空集合と対応するが，もう一つは全体集合と対応する．
一般の標準論理プログラムにおいては，全体集合もやはり解集合と認められる． しかし，PROLEG は法的推論を目的としているため，根拠が明確でない循環論法を認めない．この差を埋めるため，BAF における完全ラベリングより制約の強い意味論を与え，対応を考える必要がある．ただし，上の問題は他から支持されていない循環する支持関係のみが原因となるため，既存の完全ラベリングから大きく変更を加え謝辞
本研究は JSPS 科研費 JP17H06103 の助成を受けたものです．

参考文献[ 1 ] Amgoud, L., Cayrol, C., Lagasquie-Schiex, M. andLivet, P.: On bipolarity in argumentation frameworks. International Journal of Intelligent Systems, Volume 23,10621093 (2008).
[ 2 ] Cayrol, C. and Lagasquie-Schiex, M.: Bipolarity in argumentation graphs: Towards a better understanding. International Journal of Approximate Reasoning, Volume 54,876-899 (2013).
[ 3 ] Dung, P. M.: On the acceptability of arguments andits fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, Volume 77, 321-357 (1995)[ 4 ] Rahwan,I. and Simari,G.(eds.): Argumentation in Artificial Intelligence, Springer (2009).
[ 5 ] Satoh, K. et al.: PROLEG: the Presupposed Ultimate
Fact Theory by PROLOG Technology. Information Network
Law Review, Volume 10, 54-89 (2011).
[ 6 ] Satoh, K. et al.: On Generality of PROLEG KnowledgeRepresentation. In Proc. of JURISIN2012, 115-128 (2012).