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