Argumentation Theory - Revision history

Michael Leuschel: /* Influencing the Graphical Rendering */

2024-01-06T16:53:16Z

Influencing the Graphical Rendering

← Older revision		Revision as of 16:53, 6 January 2024
Line 121:		Line 121:
	One can influence the graphical representation of the current state in various ways.		One can influence the graphical representation of the current state in various ways.
	The user can directly define nodes and edges of the graph to be rendered.		The user can directly define nodes and edges of the graph to be rendered.
	One way to do this is by adding the following ~~lines~~ after the MACHINE section:		One way to do this is by adding the following [[Custom_Graph\|custom graph definition]] after the MACHINE section:
	<pre>		<pre>
	DEFINITIONS		DEFINITIONS

Michael Leuschel at 18:48, 20 January 2016

2016-01-20T18:48:14Z

@@ Line 78: / Line 78: @@
 </table>
 == A more elegant encoding ==
@@ Line 128: / Line 117: @@
 </pre>
 == An Event-B Version of the Model ==

Michael Leuschel: /* A more elegant encoding */

2016-01-20T18:45:09Z

A more elegant encoding

← Older revision		Revision as of 18:45, 20 January 2016
Line 129:		Line 129:


	== ~~A more elegant encoding~~ ==		== An Event-B Version of the Model ==

	Instead of using ProB Tcl/Tk you can also encode this model in Rodin, the Eclipse-based platform for Event-B.		Instead of using ProB Tcl/Tk you can also encode this model in Rodin, the Eclipse-based platform for Event-B.

Michael Leuschel at 18:41, 20 January 2016

2016-01-20T18:41:46Z

@@ Line 77: / Line 77: @@
 </tr>
 </table>
 == A more elegant encoding ==

Michael Leuschel at 18:34, 20 January 2016

2016-01-20T18:34:53Z

← Older revision		Revision as of 18:34, 20 January 2016
Line 1:		Line 1:
	Below we try to model some concepts of argumentation theory in B.		Below we try to model some concepts of argumentation theory in B.
	The examples try to show that set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory.		The examples try to show that classical (monotonic) logic with set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory.
	Alternative solutions are encoding arguments as normal logic programs and using answer set solvers for problem solving.		Alternative solutions are encoding arguments as normal logic programs (with non-monotonic negation) and using answer set solvers for problem solving.

	The following model was inspired by a talk given by Claudia Schulz.		The following model was inspired by a talk given by Claudia Schulz.

Michael Leuschel: /* A more elegant encoding */

2016-01-20T15:42:40Z

A more elegant encoding

← Older revision		Revision as of 15:42, 20 January 2016
Line 119:		Line 119:
	== A more elegant encoding ==		== A more elegant encoding ==

	Instead of using ProB Tcl/Tk you can also encode this model in Rodin.		Instead of using ProB Tcl/Tk you can also encode this model in Rodin, the Eclipse-based platform for Event-B.

	Here we have split the model into two contexts.		Here we have split the model into two contexts.
	The first one encodes the general rules for labelling (we use Camille syntax):		The first one encodes the general rules for labelling (we use Camille syntax):

Michael Leuschel: /* A more elegant encoding */

2016-01-20T15:42:13Z

A more elegant encoding

← Older revision		Revision as of 15:42, 20 January 2016
Line 149:		Line 149:
	</pre>		</pre>

	If you load this model with [[~~https://www3.hhu.de/stups/prob/index.php/~~Tutorial_Rodin_First_Step\|ProB for Rodin]], you can see the solution in the State view:		If you load this model with [[Tutorial_Rodin_First_Step\|ProB for Rodin]], you can see the solution in the State view:

	[[file:ProBRodinArgumentationState.png\|center\|\|~~350px~~]]		[[file:ProBRodinArgumentationState.png\|center\|\|450px]]

Michael Leuschel: /* A more elegant encoding */

2016-01-20T15:41:43Z

A more elegant encoding

← Older revision		Revision as of 15:41, 20 January 2016
Line 151:		Line 151:
	If you load this model with [[https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_First_Step\|ProB for Rodin]], you can see the solution in the State view:		If you load this model with [[https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_First_Step\|ProB for Rodin]], you can see the solution in the State view:

	[[file:ProBRodinArgumentationState.png\|center\|\|~~250px~~]]		[[file:ProBRodinArgumentationState.png\|center\|\|350px]]

Michael Leuschel: /* A more elegant encoding */

2016-01-20T15:41:07Z

A more elegant encoding

← Older revision		Revision as of 15:41, 20 January 2016
Line 120:		Line 120:

	Instead of using ProB Tcl/Tk you can also encode this model in Rodin.		Instead of using ProB Tcl/Tk you can also encode this model in Rodin.
			Here we have split the model into two contexts.
			The first one encodes the general rules for labelling (we use Camille syntax):
	<pre>		<pre>
	context ArgumentsAsSets		context ArgumentsAsSets
Line 126:		Line 127:
	constants attacks in out undec		constants attacks in out undec
	axioms		axioms
	@axm1 attacks ∈ ARGUMENTS ↔ ARGUMENTS // which argument attacks which other argument		@axm1 attacks ∈ ARGUMENTS ↔ ARGUMENTS // which argument attacks which other argument
	@axm2 partition(ARGUMENTS,in,out,undec) // we partition the arguments into three sets		@axm2 partition(ARGUMENTS,in,out,undec) // we partition the arguments into three sets
	@axm3 attacks∼[in] ⊆ out // if an argument is in, any attacker must be out		@axm3 attacks∼[in] ⊆ out // if an argument is in, any attacker must be out
	@axm4 attacks[in] ⊆ out // if an argument is in, anything it attacks must be out		@axm4 attacks[in] ⊆ out // if an argument is in, anything it attacks must be out
	@axm5 ∀y·(y∈out ⇒ ∃x·(x↦y∈attacks ∧ x∈in)) //if an argument y is out, it must be attacked by a valid argument		@axm5 ∀y·(y∈out ⇒ ∃x·(x↦y∈attacks ∧ x∈in)) //if an argument y is out, it must be attacked by a valid argument
	@axm6 ∀y·(y∈undec ⇒ ∃x·(x↦y∈attacks ∧ x∈undec)) // if an argument y is undecided, it must be attacked by an undecided argument		@axm6 ∀y·(y∈undec ⇒ ∃x·(x↦y∈attacks ∧ x∈undec)) // if an argument y is undecided, it must be attacked by an undecided argument
	end		end
	</pre>		</pre>

			A second context then extends the above one, and encodes our particular problem instance:

			<pre>
			context Arguments_Example extends ArgumentsAsSets
			constants A B C D E
			axioms
			@part partition(ARGUMENTS,{A},{B},{C},{D},{E})
			@example attacks = {B↦A, C↦B, D↦C, E ↦ B, E↦D}
			/* A = the sun will shine to day, B = we are in the UK
			C = it is summer, D = there are only 10 days of sunshine per year, E = the BBC has forecast sun */
			end
			</pre>

			If you load this model with [[https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_First_Step\|ProB for Rodin]], you can see the solution in the State view:

			[[file:ProBRodinArgumentationState.png\|center\|\|250px]]

Michael Leuschel at 15:35, 20 January 2016

2016-01-20T15:35:55Z

@@ Line 114: / Line 114: @@
    attacks = {B|->A, C|->B, D|->C, E |-> B, E|->D}
 END
 </pre>