\section{Our thesis}

Gamification of education and scholarship
in formal sciences
has a formal foundation with useful applications. 

Contributions of this paper:

Formulation of \sgdp and illustration with 3 examples:
optimization, different agreement, master scholar.

Concept of blame strength and how it translates to payoff.

Concept of lab reductions and how they contribute 
to problem solving.

Convergence to optimum claim.
What are  the necessary preconditions?



intrinsically motivating instruction by Tom Malone
http://mailer.fsu.edu/~jkeller/EDP5217/Library/Curiosity%20&%20Attention/Attention/Malone(1981)%20Intrinsically%20Motivating%20Instruction.pdf


\section{Positive Terminology Approach to SCG}
Terminology change:
opponent -> partner.

Create learning opportunities  for partner by creating
outcomes where the partner is contradictory. 
Contradictory bevavior is a seed for learning.
conditionally or absolutely. 

Goal of game: create learning opportunities?

\section{Negation}
We introduce a negation operator for labs that 
maps claims to claims union negated(claims).
Given a claim c, the negation of c is the claim where ...
switch P and O negate refutation predicate.
A lab is closed under negation if for every claim c,
the claim not(c) is also in the lab.

Protocol with refutation predicate
(P,O,predicate)
(O,P,!predicate)

The simple rule for claim negation is: the domain stays the same and, in the protocol, the roles of Alice and Bob are reversed and a defense is changed into a refutation.


In the following we assume that all labs are 
closed under negation.

refute(c,P,O)) = defend(!c,O,P)
Defending a claim c has the same difficulty as refuting its complement !c.

negation is needed
agree(c)
dispute(c)
agree(!c)
strengthen(c,c')

agree(!c) = dispute(c) ??


\section{The \sgdp\  with Applications}

In paper \cite{scg-def} we use the following game
design pattern called \sgdp.

Using Game Goal and Blame Assignment to systematically
Design the Payoff Function

In our game design problems
(1) there is a game design goal that defines what the game should achieve
(2) there are blamable moves that are considered non-productive with respect to the design goal.

The design goal is then translated into a blame assignment that matches the design goal.

Finally, the blame assignment is translated into a payoff function that is fair, sound and competitive with respect to the blame assignment.

Fairness means that if S is not blamed,
payoff(S)>=payoff(!S).
(!S is the other scholar.)

Soundness means that if S is blamed then
payoff(S)<payoff(!S).
%S will have a negative payoff.
Or soundness means that if S is blamed then there is
a chance that S will have a negative payoff.
(There are different variants of soundness depending on
the different kinds of blamable moves.)

Competitiveness means that the payoff is higher for the winner.

The first important goal in SCG is not to contradict yourself. 
You contradict yourself, if you make a decision which
has an implied assumption but then you don't satisfy that 
assumption.
For example, if you decide to dispute a claim, the implied
assumption is that you will refute it successfully.
If you don't, you contradict yourself.
See Figure \ref{GameTreeTableOpt} for all 5 ways to 
contradict yourself in SCG with Optimization. 

A second important goal is not to propose
false claims. You risk being caught when you do.

\subsection{Application to Optimization Labs}
Useful for learning: want to converge to optimum claim.

\subsubsection{Blame and Payoff Table}

\ref{CompleteTable} explains the issues described in
the following paragraph:

Regarding blame, blame is a technical term that we carried over from PL. The point is that we want to formally verify that our game design isn't futile especially that a part of the final game tree is provided by lab designers. Our approach consists of labeling certain edges / nodes of the game tree with additional properties (for example that an edge represents a blamable action or that we cannot distinguish between actions taken at a particular node). Then assert certain generic properties (that involve those newly added labels) about the the overall tree. These generic formal properties define what makes the game interesting (or non futile). We couldn't find such generic definitions of game interestingness in the literature. And would like to get your input on that.
(from Ahmed's email)

From where come the blamable actions?
They are implied by the decisions made. Each decision
has an expected result: When you are accepted by 
a PhD program, people expect that you get your PhD.
When you agree with a claim, you are expected to defend 
it successfully.
When you propose a claim, you are expected to defend it successfully or to refute a stronger claim.
When you dispute a claim, you are expected to refute it.
When you strengthen a claim, you are expected to defend
the strengthened claim.

If you fail to meet the expectation, you are called
contradictory and you get blamed.

If you fail to meet the expectation, you get blamed.
Your goal in the game is to teach your opponent by
bringing him or her into a situation where it gets 
blamed absolutely (column oB) or conditionally (columns
fB and nB).

In Figure \ref{CompleteTable}, 
in columns fB and nB we give a row number 
which indicates how to translate conditional blame 
into a positive payoff for the opposer.
The table has 3*6+1=19 rows.  
If a false claim is proposed, the best action is
to dispute it and to successfully refute it (row 8:
the header row is row 1).
If a non-optimal claim is proposed, the best 
action is to strengthen it and to defend
the strengthened claim (row 15).

%add a new claim property: OT for optimal

add a new decision possibility for dec: s = strengthen

update blame justification

size of table:
Consider the table
\ref{GameTreeTableOpt} which describes the generalization
for optimization.

This table seems very useful as we see all the information in one table not spread out between a game tree and a table.

A claim is either true or false.
A true claim should be optimum. 

Figure \ref{AllLearning} describes all learning opportunities.
There are two levels of learning opportunities:
level 1 in column 1B and level 2 in column 2B.
Blame is not only assigned for claim choices (proposing a false 
or non-optimal claim, level 1) but also for decisions (e.g., disputing
an optimal claim, level 2). 

1B: row number that blames choice by forcing loss

2B: row number that blames decision by showing better decision that avoids loss.
We show the line number for the case where there is an improvement
if a better decision is made.

Column 2B:

Ta is blamed because TssO (row 15)is guaranteeing a win for O.

Td is blamed because TssO is guaranteeing a win for O.

T-optd is blamed because T-OptasO is avoiding a loss for O.

T-opts is blamed because T-OptasO is avoiding a loss for O.

Ahmed talks about CTL expressible properties that tree must have.
Can they be expressed with such row numbers?

%dependencies:  for OT, a and s									
%OT rP	P prevented agreement or strengthening successfully								
%OT sO	O agreed or strengthened successfully								
%
%
%The table can be simplified by combining:
%
%OT a sO and T a sO
%
%and by combining
%
%OT a rP and T a rP

What are the constraints that must hold?
They are in Figure \ref{SCGCSPFSCOPT}.

\subsection{Application to Agreement with two Refutation Games}
Has first the flavor of a regular dispute.
\subsubsection{Blame and Payoff Table}

add a second out2 column used for agreement only.

see Figure \ref{ImprovedAgreement}.
The agreement protocol consists of two applications of the refutation
protocol with the provision that all solutions
are only revealed at the end of the protocol.

advantages

Two applications of the refutation protocol with reversed
roles leads to more testing of claims and scholars.
The game is more balanced: P and O are blamed in the oB*
columns on two outcomes while before only O could be
blamed in the oB column.

disadvantages

The cost is higher.

Casper: no negative payoff. Exception both get
a negative payoff:

\begin{verbatim} 
0   0
1  -1
-1  1
-1 -1

becomes 
0   0
1   0
0   1
a   a
where a = -1/4.
\end{verbatim} 
\subsection{Application to Perfect Labs}

We call a lab perfect if the lab designers know which claims are true and which are false.
In this case the blame can be targeted more directly
because there is no uncertainty about whether
a claim is true or false. This applies often 
during learning where the lab designer (teacher)
has more knowledge than the students.

See Figure \ref{MasterScholar}.
Is the payoff fair and sound? Complete the table.
There is a need to have a weight on the blame
(strength of the learning opportunity).



\subsubsection{Blame and Payoff Table}
