Argumentation Theory

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. Alternative solutions are encoding arguments as normal logic programs and using answer set solvers for problem solving.

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

The model below represents the labelling of the arguments as a total function.

MACHINE ArgumentationTotFun
SETS
 ARGUMENTS={A,B,C,D,E};
 STATUS = {in,out,undec}
CONSTANTS attacks, label
PROPERTIES
  attacks : ARGUMENTS <-> ARGUMENTS  /* which argument attacks which other argument */
  &
  label: ARGUMENTS --> {in,out,undec} & /* the labeling function */
  !(x,y).(x|->y:attacks => (label(y)=in => label(x)=out)) &
  !(x).(x:ARGUMENTS => (label(x)=out => #y.(y|->x:attacks & label(y)=in))) &
  !(x,y).(x|->y:attacks => (label(y)=undec => label(x)/=in)) &
  !(x).(x:ARGUMENTS => (label(x)=undec => #y.(y|->x:attacks & label(y)=undec)))

 &
  // here we model one particular argumentation graph
  // 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
  attacks = {B|->A, C|->B, D|->C, E |-> B, E|->D} 
END