namespace http://mathhub.info/ALMANAC/Context-Graph ❚
/T Basic example of a Dung abstract argumentation framework interpreting theories as arguments and views as attacks ❚
theory a = ❚
theory b = ❚
theory c = ❚
view a_attacks_b : ?a → ?b =
❚
view b_attacks_a : ?b → ?a =
❚
// view c_attacks_a : ?c → ?a =
❚
// Doing Semantics: For semantics, one would have to teach MMT to compute the different semantics
based on the views between theories. Alternativey, this could be done in the graph viewer.❚
// A larger example: ❚
theory A = ❚
theory B = ❚
theory C = ❚
theory D = ❚
theory E = ❚
theory F = ❚
theory G = ❚
view A_attacks_B : ?A → ?B =
❚
view B_attacks_A : ?B → ?A =
❚
view G_attacks_F : ?G → ?F =
❚
view E_attacks_F : ?E → ?F =
❚
view F_attacks_D : ?F → ?D =
❚
view D_attacks_C : ?D → ?C =
❚
view C_attacks_A : ?C → ?A =
❚
view C_attacks_B : ?C → ?B =
❚
/T A little bit more. First a metatheory: ❚
theory TrueFalse : ur:?LF =
prop: type ❙
true: prop ❘#T ❙
false: prop ❘#F ❙
bot: prop ❘ # ⊥ ❙
impl: prop ⟶ prop ⟶ prop ❘ # 1 implies 2 ❙
and: prop ⟶ prop ⟶ prop ❘ # 1 and 2 ❙
ded: prop ⟶ type ❘ # ⊦ 1 ❙
axiom: ⊦ (T and F implies ⊥) ❙
❚
theory TND : ur:?LF =
prop: type ❙
neg: prop ⟶ prop ❘ # ¬ 1 ❙
impl: prop ⟶ prop ⟶ prop ❘ # 1 implies 2 ❙
ded: prop ⟶ type ❘ # ded 1 ❙
bot: prop ❘ # ⊥ ❙
LEM1: ded {A:prop}(A implies (neg (neg A))) ❙
LEM2: ded {A:prop}(neg (neg A) implies A) ❙
❚
/T Now the contentious propositions:❚
theory props =
include ?TND ❙
fact1: prop ❙
fact2: prop ❙
❚
theory one =
include ?TrueFalse ❙
True: ⊦ T ❙
❚
theory two =
include ?TrueFalse ❙
False: ⊦ F ❙
❚
view one_attacks_two : ?one → ?two =
include ?TrueFalse = ?TrueFalse ❙
/T True = False
/T The following line characterises the attack: one and two disagree allow to prove contradicting statements. Hence one attacks two on fact1 (or vice versa: these semantics for attack don't tell us enough yet to determine the correct direction of the arrow). Allowing a view to have this could e.g. involve a replacement of "=" by some contradiction operator. Note also the different between finding a view that yields a contradiction and proving that no non-contradictory view /theory-morphism is possible between the two theories.❙
/T supports_fact1 = attacks_fact1 ❙
❚
/T Another semantics for attack based on includes, views and conflict theories❚
theory common_ground =
include ?TND ❙
X : prop ❙
Y : prop ❙
❚
theory conflict =
include ?TND ❙
C: prop ❙
A: ded C ❙
B: ded (C implies ⊥) ❙
❚
theory three =
include ?TND ❙
X : prop ❙
Y: prop ❙
ass1: ded X ❙
ass2: ded (X implies ¬Y) ❙
❚
theory four =
include ?TND ❙
Y : prop ❙
ass3: ded Y ❙
❚
theory oneandthree =
include ?three ❙
include ?four ❙
❚
view three_attacks_four : ?conflict → ?oneandthree =
include ?TND = ?TND ❙
C = X ❙
/T A = ass1 ❙
/T B = ded X implies ⊥ ❙
A = ass1 ❙
❚