\section{Introduction}
Popper, one of the most prominent philosophers of science
of the previous century, promoted in
``Conjectures and Refutations'' the idea that each hypothesis
should have a description how it could be refuted, and that
scientific knowledge grows through the introduction of 
refutable hypothesis followed by intensive testing of their
correctness.

We designed the Scientific Community Game (SCG) to encourage
scholars to put as much effort and intelligence as possible into proposing
claims that are hard to falsify as well as into attempting to refute those claims.
% (2) focus research and development efforts on a particular family
% of falsifiable claims.
 %Benefits
The gamification of science that we propose has several {\bf benefits}:
(1) We make scientific activity available to a wider audience. Trying to refute a claim is a simple activity.
(2) We get psychological advantages: playing the game is fun and leads to the discovery of what is known within the current group of players.
(3) We make it easy to expose claims to refutation attempts, which leads to better science in the long run \cite{nla.cat-vn1027910}.
(4) The lab definition mechanism of the SCG makes it easy to focus a group of people on a specific problem.
(5) Popper's ideas become applicable to claims in any formal science not only to complex scientific theories.
 
\subsection{SCG in a Nutshell}
In the SCG, a lab consists of a set of refutable claims~\cite{nla.cat-vn1027910}.
Scholars take on the roles of proponents and opponents of the claims in the lab.
Opponents attempt to refute claims against proponents. 
A refutation attempt initiates an orderly dialog between the proponent and opponent,
which induces collaborative behavior.
In the SCG, successfully refuting a claim against the claim's proponent does not mean that the claim is false. 
It only means that the proponent might not have the skills to defend the claim.
The labs are self-evaluating in that there is no need of a third party
to evaluate the contributions of the scholars: the proponent
and opponent evaluate each other fairly.
% This is enforced by the SCG-level generic game rules and by the refined 
% lab-level more specialized rules.

There are two classes of SCG users, lab designers and scholars (players). 
% The SCG defines generic rules for a
% scientific community and
% lab designers specialize those rules to a specific domain
% which in turn defines the tasks to be performed by the scholars.
\begin{itemize}
\item
Lab designers have a problem they want to focus scholars on solving through specializing SCG.
The role of lab designer can be played by a researcher who needs a specific problem solved or an educator
who wants her students to practice what they were taught.
Lab designers define a few sets and functions that define the
problem to be solved. As return on their investment
they get a lab where scholars are invited to participate
to solve the problem.
Defining a lab can be viewed as writing a program for the global brain 
\cite{Bernstein:2012:PGB:2160718.2160731}.

\item
Scholars inhabit a lab, either because they are enticed by an educator
or because they have good skills to solve the problem
defined by the lab. A scholar has the opportunity to influence
the quality of the knowledge base
and the quality of the lab procedures.
Scholars are evaluated in the lab based on the quality of their contributions
compared to the contributions of their peers.

The role of scholar can be played by a human or an avatar
(software). The avatar variant works only for labs that
are sufficiently well understood.
\end{itemize}



\subsection{SCG Applications}
SCG has several {\bf applications}, including:
\begin{enumerate}
  \item problem solving and research in formal science. Funding agencies, such as NSF, define, in collaboration
		with interested researchers, labs that define the problem
		to be solved. Through playing the game, NSF builds a knowledge base of refutable claims and refutation attempts.
		Furthermore, the self-evaluating nature of SCG will fairly evaluate the contributions of scholars
		and the collaborative nature will lead to productive team work. 
		Newcomers can contribute by participating in a long-running lab (dozens of years).
  \item teaching (traditional, online and massively open online) courses in STEM areas. 
  		To teach a particular problem solving skill, we design a lab for the problem.  
  		Playing SCG challenge the students' self-image about their ability to solve the lab's problem.
  	    Thus, encouraging students to acquire the desired problem solving skill.
  	    The self-evaluating nature of SCG helps lifting much of the evaluation from the teacher and allows
  	    stronger students to give precisely targeted feedback to weaker students.  
%   		To teach a specific skill, we design a lab which encourages
% 		scholars to acquire that skill to perform well in the lab.
% 		For teaching, it is important to use a payoff function
% 		which reduces the competitiveness of the game
% 		and which enhances the collaborative nature. 
% 		Good students
% 		become effective teachers to the weaker students.
% 		Our experience has been that optimization labs work best for teaching.
  \item software development for computational problems. A computational task is defined by a lab where the role
		of a scholar is played by an avatar (software).
		Competitions are held, and the winning avatars will contain
		the best (within this group of competing avatars) 
		algorithms for the computational task.
\end{enumerate}

\subsection{Contributions}

The main contribution of this paper is a definition of SCG, a generic game for the
Popperian Scientific Method \cite{nla.cat-vn1027910}. 
The SCG definition in this paper presents an abstraction of
 our publicly available implementation \cite{SCGCourt}. 
 
% A secondary contribution of the paper is a formalization of refutations
% based on earlier work in logic (predicate logic and its generalizations).

%Properties
% We also show that the SCG has several {\bf desirable properties} 
% (see section \ref{propertiesSection}).% which make the game interesting.

A second contribution of this paper is an analysis of SCG that shows that it is
consistent with its design goals, and it has several desirable properties that make the
game interesting. 
  
%We call the players scholars because the game is about
%making scientific or technical claims and defending them.
%  We focus on formal sciences
%  although the idea
%  applies to both formal sciences and other sciences.
%  Unlike other sciences, the formal sciences are not concerned with the
%  validity of claims based on observations in the real world,
%  but instead with the properties of formal systems based
%  on definitions and rules.
%  Examples of formal sciences are
%  logic, mathematics, theoretical computer science,
%  information theory, systems theory, decision theory, statistics.
% For a longer list, see \cite{Franklin1994-FRATFS}.
% Natural sciences for which adequate simulators exist become formal sciences from the point of view of the SCG.

% {\bf From Ahmed
% It's probably advisable for us to rationalize the game tree design as well.
% 
% Also we can probably frame SCG as a game designed to encourage constructively-solvable disputes about a predefined set of claims. The reason we'd want to encourage those constructively-solvable disputes is that they help advance and focus the scientific discourse and learning.
% }


\subsection{Organization}
This paper is organized as follows: In section~\ref{BinaryGameDefinitionSection} we define binary SCG while 
in section~\ref{BeyoundBinarySCGSection} we introduce SCG competitions that build on binary SCG.
In section~\ref{DisscussionSection} we describe SCG from the perspective of current game design models. 
In section~\ref{propertiesSection} we analyze the binary game and show that it has properties that make the game interesting. 
In section~\ref{ExperienceSection}, we present our experience with SCG.
In section~\ref{RelatedSection}, we present some of the related work. 
In section~\ref{FutureWorkSection} we present some of our future work. 
Section~\ref{ConclusionSection} concludes the paper.


%END NEW BEGINNING
%
%% done by grammarly
%The Scientific Method has not yet been implemented
%as a generic software tool that can be customized for various 
%domains.
%We present our design of such a generic tool
%to develop new knowledge and call it the Scientific
%Community Game (SCG).
%SCG applications range from research/problem solving 
%(building knowledge bases by refuting and defending claims) to teaching (traditional, online and massively open online) courses
%in STEM areas.
%There have been several calls to use more science in computer science and programming
%\cite{Denning:2005:CSS:1053291.1053309,ScientificMethodProgramming}.
%The concept of labs that we introduce in this paper makes it is easier
%to organize small or large scientific communities that apply
%the Scientific Method.
%
% While this paper defines the SCG, there are separate papers planned that describe various applications of the SCG.
% \begin{itemize}
% \item{SCG for Funding Agencies}
% 
% %checked by grammarly
% Funding agencies, such as NSF, define, in collaboration
% with interested researchers, labs that define the problem
% to be solved. The self-evaluating nature of the SCG will fairly
% evaluate the contributions of scholars and the 
% collaborative nature will lead to productive team work.
% Newcomers can contribute by participating
%  in a long-running lab (dozens of years).
% 
% \item{SCG for Software Development}
% 
% A computational task is defined by a lab where the role
% of a scholar is played by an avatar (software).
% Competitions are held, and the winning avatars will contain
% the best (within this group of competing avatars) 
% algorithms for the computational task.
% 
% \item{SCG for Teaching}
% 
% To teach a specific skill, we design a lab which encourages
% scholars to acquire that skill to perform well in the lab.
% For teaching, it is important to use a payoff function
% which reduces the competitiveness of the game
% and which enhances the collaborative nature. Good students
% become effective teachers to the weaker students.
% Our experience has been that optimization labs work best for teaching.
% \end{itemize}


% done by grammarly
% In SCG, claims are organized into labs where they are exposed to refutation attempts


% 
% %\newpage
% \subsection{SCG Users}
% 
% There are two levels of SCG users:
% Lab designers and scholars (players). The SCG defines generic rules for a
% scientific community and
% lab designers specialize those rules to a specific domain
% which in turn defines the tasks to be performed by the scholars.
% \begin{itemize}
% \item
% Lab designers have a computational problem they want
% to have solved. The role of lab designer can be played by
% a researcher who needs a specific problem solved or an educator
% who wants her students to practice what they were taught.
% Lab designers define a few sets and functions that define the
% problem to be solved. As return on their investment
% they get a lab where scholars are invited to participate
% to solve the problem.
% Defining a lab is like writing a program for the global brain 
% \cite{Bernstein:2012:PGB:2160718.2160731}.
% 
% \item
% Scholars inhabit a lab, either because they are enticed by an educator
% or because they have good skills to solve the problem
% defined by the lab. A scholar has the opportunity to influence
% the quality of the knowledge base
% and the quality of the lab procedures.
% Scholars are evaluated in the lab based on the quality of their contributions
% compared to the contributions of their peers.
% 
% The role of scholar can be played by a human or an avatar
% (software). The avatar variant works only for labs that
% are sufficiently well understood.
% \end{itemize}


\section{Binary Game Definition}
\label{BinaryGameDefinitionSection}
We first define the binary SCG which is the building block for competitions.
The game is played between two scholars (players), Alice and Bob, disputing the correctness and 
optimality of claims about a particular domain. 
We define the binary SCG through its extensive-form
(or tree-form) representation which
is a common representation in game theory \cite{doi:10.2200/S00108ED1V01Y200802AIM003}. 
We start by giving some auxiliary definitions for {\it Domain}, 
{\it Refutation Protocol}, {\it Lab}, {\it Claim} and {\it Refutation Game} that we eventually use
for defining the Binary SCG.

% To define the moves, we need a few sets and functions which make up 
% what we call a lab where experiments and measurements may be performed
% in a specific domain.
% A lab defines a common ontology between players and consists of 
% a domain which defines a set of instances and corresponding solutions.

\subsection{Domain}

A {\it Domain} consists of:
\begin{enumerate}
  \item a set {\it Instance} of (problem) instances, 
  \item a set {\it Solution} of (problem) solutions,
  \item  a predicate {\it valid(i : Instance, s : Solution) : Boolean} that holds when
the solution {\it s} is valid for the instance {\it i}, and
  \item a function {\it quality(i : Instance, s : Solution) : Real} that returns a real 
  number representing the quality of the solution {\it s} to the instance {\it i}. 
\end{enumerate}

When designing a domain the {\it valid} function should be as lax as possible such that valid solutions 
for any problem can be found with minimal to no intelligence. The reason is that failing to provide a {\it valid} 
solution is used as an indicator that a player (which can be an avatar) is out of order and that it should be kicked 
out of the lab immediately. It should also be kept in mind when designing the {\it quality} function that the game 
interprets higher quality as being better. 
   
Examples of domains include, the domain of CNF Satisfiability where {\it Instance} is 
the set of CNF formulae, {\it Solution} is the set of variable assignments to booleans.
A solution {\it s} is valid for an instance {\it i} if and only if {\it s} provides a boolean value for
all variables mentioned in {\it i}. A potential definition of {\it quality(i,s)} is the fraction of clauses in {\it i} 
satisfied by {\it s}.

When there are multiple valid solutions for a given problem, the $quality$ function is used to discriminate between them.
For example, for the domain where $Instance$ is the set of sequence alignment and $Solution$ is the set of all sequence 
alignment algorithms such as Smith-Waterman and BLAST,\ldots etc, we could be concerned with full sequence alignment in 
which case, Smith-Waterman might have a higher quality. If we are interested in trading some accuracy for speed, BLAST 
might be of a Higher quality.

\subsection{Refutation Protocol}
% The refutation protocol decides one's performance when 
% refuting or defending
% a particular claim.
% All claims in a lab share the same refutation protocol.
% % with a scholar in a given lab. 
% It provides opportunities for learning
% and trying to figure out how the other scholar ``thinks''.
% It defines the scientific discourse to be used to ``test'' a claim.
% 
% The refutation protocol
% has three arguments: a claim $c$ and a Proponent and an Opponent and
% consists of a list of steps.
% %followed 
% %by a refutation predicate which receives the data as arguments.  
% The list of steps defines 
% data (instances in a subset of {\it Instance} and solutions in set {\it Solution}) that are 
% given to the refutation predicate.
% 
% Protocols are defined by the following grammar:
% 
A refutation protocol is a sequence of actions to be taken by two players, a proponent and an opponent of a particular claim, 
in order to resolve a dispute about whether the claim holds or not. The actions can be either to provide an instance or to 
provide a solution to a particular instance. Protocols can be defined by the following grammar:
%(// is the comment symbol)
\begin{verbatim} 
ProtocolSpec =  <steps> CommaList(Step).
Step = <actor> Actor <action> Action.
Actor = Proponent | Opponent.
Proponent = "P".    
Opponent = "O".
Action = ProvideAction | SolveAction.
ProvideAction = "I" "[" <instanceId> int "]".
SolveAction = "S" "[" <solutionId> int "]" 
  "of" <instance> ProvideAction.
\end{verbatim}
%// solve the instance provided in 
%// step # stepNo.
%// stepNo is 0-based.

An example of a protocol is \(P:I[0], O:S[1]\ of I[0]\) in which the proponent provides an instance
named \(I[0]\) and the opponent provides a solution named \(S[1]\) for the instance \(I[0]\).

% A protocol together with the refutation predicate is well-formed, if
% every {\sf ProvideAction} is used by at least one later {\sf SolveAction} 
% or the refutation predicate and
% every {\sf SolveAction} refers (through the step number) to a {\sf ProvideAction}.
% The output of every {\sf SolveAction} must be used in the refutation predicate.
% %"Used in the refutation predicate" means accessible through the parameter list.
% %A protocol is well-formed, if
% %every ProvideAction is used by at least one later SolveAction and the predicate and
% %every SolveAction must refer to a ProvideAction.



\subsection{Lab and Claim}
Labs play a central role in SCG. SCG games are played in the context of a particular lab. 
A lab focuses the scientific discourse of games played in it through defining a family of 
claims about a particular domain. The claims in a lab have the same structure and only differ
in the claim parameter values. Labs require a great care to define and effectively resemble a 
declarative specification of a (human) computation  \cite{Bernstein:2012:PGB:2160718.2160731} 
that separates true from false claims in 
the lab and also finds the optimal claims in optimization labs.

% A lab is centered around a refutation predicate (the main concern of the lab).
% See Fig. \ref{SCGstructure} (left side, middle) for a summary of a lab.

A {\it Lab} consists of:
\begin{enumerate}
  \item a $Domain : d$ that gives a context for claims defined in the lab; 
  \item a refutation protocol $proto : Protocol$, used to resolve disputes regarding the correctness of claims;
  \item a claim structure $Claim$ consisting of:
  		\begin{enumerate}
  			\item a number of claim parameters;
  			\item an instance set predicate $isp(i : d.Instance) : Boolean$ defining a family of instance sets. 
        			Each set in the family is a subset of {\it d.Instance} and is chosen by claim parameter values. 
        			The intuition is that a claim $c$ asserts a property about the set $\forall i \in d.Instance : c.isp(i)$.
%         			 Therefore,
%         			all instances exchanged while defending a claim must be in this set.
        	\item   a refutation predicate $p(I$ $:$ $d.Instance[],$ $S:$ $d.Solution$ $[]) : Boolean$ 
        			defines the property that the claim asserts about the family of sets defined by $isp$.
%   					used to determine whether a claim $c$ is supported (when the predicate returns true) based on the instances $I$
%   					and solutions $S$ acquired through the refutation protocol. 
  					The protocol together with the refutation predicate are well-formed, if
					every {\sf ProvideAction} is used by at least one later {\sf SolveAction}
					or the refutation predicate and
					every {\sf SolveAction} refers (through the step number) to a {\sf ProvideAction}.
					The output of every {\sf SolveAction} must be used in the refutation predicate.
  					\item a predicate $stronger (c_2 : Claim) : Boolean$ defining a partial order on claims in the lab.
  					\item a function $distance (c_2 : Claim) : Real$ defining the distance between two claims in the lab provided that
  							the one of the claims is stronger than the other.
  		\end{enumerate}
 \end{enumerate}
 
Consider a lab with the following protocol instance
\(P:I[0], O:S[1]\) of \( I[0].\)
A claim $c$ in this lab intuitively means:
``I, the proponent, can give an instance $I[0]$ where $c.isp(I[0])$ holds, such that
for any solution {\it S[1]} of {\it I[0]} given by you, the opponent, 
where {\it valid(I[0],S[1])} holds, the refutation predicate $p(I, S)$ holds.''.
This claim can also be expressed as a mathematical statement about the underlying domain as:
``There exists an instance {\it I[0]} where $c.isp(I[0])$ holds, such that
for all solutions {\it S[1]} of {\it I[0]} where {\it valid(I[0],S[1])} holds,
the refutation predicate $p(I, S)$ holds.''. 
In order to support this claim, the proponent has to deliver $I[0]$
and opponent has to deliver {\it S[1]} in a resource constrained environment.

If we append the following protocol step to the end of the above protocol
\(P: S[2]\) of \(I[0]\)
and define the refutation predicate to be:
$p(I,$ $S)$ $=$ $(Lab.d.quality(S[2],$ $I[0])$ $\ge$ $Lab.d.quality(S[1],$ $I[0]))$,
we get a very different kind of claim. It says
that proponent is at least as good as opponent in solving instances
in the given lab. Which is a statement about the performance of players rather than
about the underlying domain.

\subsubsection{Classification of Claims and Labs}
%Now the claim definition is complete.
We define a claim to be {\bf true} if it has a support strategy for the proponent. This means that,
for true claims, the proponent can always avoid refutations.
We define a claim to be {\bf false} if it has a refutation strategy for the opponent, i.e.,
the opponent can always succeed in refuting.
We define a claim to be {\bf indeterminate} if it has neither a defense nor a refutation strategy.

We classify labs into {\bf optimization}, {\bf standard},and {\bf bivalent} labs.
Optimization labs have no restrictions. Standard labs are where claims are not comparable for strength 
(i.e. the $stronger$ predicate is defined to be $false$). Bivalent labs are a special case of standard labs with
no indeterminate claims.
% 
%  
% 
% labs can be classified into the following three classes:
% \begin{enumerate}
%   \item Standard labs : the $stronger$ predicate is defined to be $false$ in standard labs. The goal of playing SCG in a standard lab is 
%   		to separate true, and false claims. 
%   \item Bivalent labs : is a special case of the standard lab that has no indeterminate claims.
%   \item Optimization labs : the $stronger$ predicate is not defined to be $false$. The stronger predicate, however, must satisfy the condition
%         that there is no true claim that is stronger than a false claim. This captures the intuition that there is a critical point at which 
%         claims transition from being true to being false. The goal of playing SCG in an optimization lab is
%         to find critical points.  
% \end{enumerate}

\subsection{Refutation Game}
 To attempt a refutation of a given claim $c$, both the proponent $pro$ and the opponent $opp$ of the claim enter into a 
 refutation game $refute(c : Claim, pro : Scholar, opp : Scholar)$.
 
 The refutation game consists of
	an exchange of instances and solutions as defined by the protocol $c.Lab.proto$ where the proponent $P$ and opponent $O$ in 
    the protocol are bound to the scholars $pro$ and $opp$ respectively. The exchanged instances must be in the set 
    $\forall i \in c.d.Instance : c.isp(i)$. A solution $S[n]$ for instance $I[m]$ must be valid for that instance.
     i.e. $c.d.valid(I[n], S[m])$ must hold.
     The refutation predicate is used to decide the winner of the refutation game. If the $c.p(I, S)$ holds, the proponent has successfully 
     supported the claim and wins. Otherwise, the opponent has successfully refuted the claim and wins. $I$, $S$ refer to the
     instances and solutions exchanged during the refutation game.
  	 As a general rule, solutions are all kept secret until protocol
	 evaluation. When a scholar provides a solution she does not know about solutions provided by the other scholar.

  
% All claims in SCG are disputable. To dispute a claim $c$ proposed by Alice, Bob engages Alice in a 
% refutation game centered around $c$. A refutation game for a claim $c$ is played between two scholars one 
% taking the role of the proponent $pro$ and the other
% taking the role of the opponent $opp$, denoted as $refute(c : Claim, pro : Scholar, opp : Scholar)$, consists of 
% 	an exchange of instances and solutions as defined by the protocol $c.Lab.proto$ where the proponent and opponent in 
%     the protocol are bound to the scholars $pro$ and $opp$ respectively. The exchanged instances must be in the set 
%     $\forall i \in c.d.Instance : c.isp(i)$. A solution $S[n]$ for instance $I[m]$ must be valid for that instance.
%      i.e. $c.d.valid(I[n], S[m])$ must hold.
%      The refutation predicate is used to decide the winner of the refutation game. If the $c.p(I, S)$ holds, the proponent has successfully 
%      supported the claim and wins. Otherwise, the opponent has successfully refuted the claim and wins. $I$, $S$ are the
%      instances and solutions exchanged during the refutation game.

\subsection{Binary SCG}
% We use a summary tree (see Figure \ref{SCGextensive})
% to summarize the tree defining binary SCG.
% There are three kinds of edges in the summary tree
% \begin{enumerate}
%   \item standard edges with a label which gives a decision action (thin blue),
%   \item multi edges with a label which is a set from which an element is chosen 
% by the action (thick dashed blue), and
%   \item path edges, which summarize refutation games (thick solid red).
% \end{enumerate}
% % A path edge describes a tree where the nodes are labeled by
% % either Proponent or Opponent and the edges are labeled by
% % provide (an instance) and solve (an instance) actions. 
% % A provide action edge itself is a multi edge which is labeled by a set of instances.
% % Path edges always enter leaves.
% % {\sf any} nodes are either labeled by Proponent or Opponent, depending on the
% % refutation protocol.
% % 
% % The summary tree defining the SCG binary game
% % has 7 edges (2 standard, 2 multi and 3 path edges) and 8 nodes of which 3 are leaves which give the payoffs
% % for the scholars.
% The context for the tree is a lab, in other words, the definition is parametric
% and applicable to an infinite number of games.
% The instantiated trees are typically huge because there might be many claims,
% instances and solutions in a lab.

% The binary SCG consists of two phases: the propose-classification phase
% (top two levels of game tree) followed by a refutation game 
% (third and lower levels of game tree).

The first move is performed by the scholar taking the role of the proponent, 
and it is to propose a claim $c$ from the claims in the lab. 
By doing so, the proponent asserts that $c$ is a true claim that 
there is no other claim in the lab that is stronger. 
In Figure~\ref{SCGextensive}, the first move is denoted by a thick dashed blue 
line to indicate that it summarizes a tree with single edge branches, an edge for each possible claim $c$.

The second move is performed by the opponent, and it is to decide whether to:
\begin{enumerate}
  \item dispute the correctness of $c$, denoted {\it disputeD(c)}, or to
  \item dispute the optimality of $c$. In this case, the opponent must provide a stronger claim $c'$. This decision is denoted {\it strengthenD(c, c')}, or to
  \item agree with $c$, denoted {\it agreeD(c)}.
\end{enumerate}

Based on the second move, the proponent and the opponent enter into a different refutation game, which is denoted by a thick solid red line to indicate
that it summarizes a tree with branches of arbitrary length. This is consistent with our design goal of encouraging refutation attempts.
If the second move is {\it disputeD(c)}, the refutation game is $refute(c,$ proponent$,$ opponent $)$. 
If the second move is {\it strengthenD(c, c')}, the refutation game is $refute(c',$ opponent$,$ proponent $)$.
If the second move is {\it agreeD(c)}, the refutation game is $refute(c,$ opponent$,$ proponent $)$. 
Even though, there is no dispute, the two players engage in a refutation game to test whether 
the opponent is indeed able to support $c$ or it is only trying to avoid entering into a dispute with the proponent over $c$.

Scholars must make their moves within a given resource (time, space, \ldots etc) limit. 
The winner of the binary SCG, is the scholar that achieve the highest payoff. Payoff is discussed in section~\ref{payoff}.

% The {\bf first} choice made in the SCG binary game tree of the extensive
% form representation is to choose a claim from {\it Claim}.
% See Fig. \ref{SCGstructure} (left lower corner) for a summary of a claim.
% A claim consists of a name, the proponent, the lab
% to which it belongs and the claim
% parameter values that, e.g., select a specific instance set.

%A claim consists of an instance of the structures
%introduced above for a lab: it has an instance set predicate, a protocol and a refutation predicate.
%

%definition of {\it Instance} and
%{\it Solution},
%a protocol and a rational number.
%The rational number has the meaning of a quality 
%that can be achieved when solving a constructive 
%task that precisely defines the allowed inputs (\( i \in {\it Instance}\))
%and the allowed solutions (\(s \in {\it Solution}\) satisfying {\it valid(i,s)}) with
%\(  {\it quality} (i,s) \).

%In an earlier version of the Scientific Community Game,
%we used the term ``challenge'' instead of ``claim.''
%A claim challenges you to refute it.

%We need functions to compare claims and compute their distance.  Function \( {\it stronger} (c_1,c_2) \) 
%checks for two claims
%\(c_1, c_2 \)
%in {\it Claim} whether
%claim \(c_1\) is stronger than claim \(c_2\).
%For some labs, predicate {\it stronger} always returns false.
%We need a function to compute the distance between claims:
%The function \( distance(c_1,c_2) \) has the property: if \(stronger(c_1,c_2)\) 
%then \(distance(c_1,c_2) > 0.\)
%Distance is used for managing payoff:  the stronger the second claim, the higher the payoff.
%

% The {\bf second} choice in the SCG binary game tree is of a different nature:
% to decide
% whether (to try) to {\it refute}, {\it strengthen}, or {\it agree} with the claim.
% Depending on the choice made, the refutation protocol is
% executed with the appropriate arguments.
% The functions {\it strengthen} and {\it agree} are also reduced to {\it refute}.
% 



% When an instance $\in \rm{Instance}$ is chosen

%The sequencing of the data collection together with the 


%to choose from.

%The extensive
%\begin{verbatim}
%http://en.wikipedia.org/wiki/Extensive-form_game
%\end{verbatim}
%
%Shoham, Yoav; Leyton-Brown, Kevin (2009), Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations, New York: Cambridge University Press, ISBN 978-0-521-89943-7. A comprehensive reference from a computational perspective; see Chapter 5. Downloadable free online.
%
%http://www.masfoundations.org/mas.pdf

%We call the players scholars because the game is about
%making scientific or technical claims and defending them.

% The extensive-form representation of the SCG binary game is given by
% (1) Two scholars, called Proponent (female) and Opponent (male).
% (2) For both scholars, every opportunity they have to move. The sequencing of moves is important.
% (3) What each scholar can do for each of their moves. They can choose from some
% set, e.g., claims, instances and solutions or make a decision about 
% classifying claims.
% (4) What each scholar knows for every move. 
% (5) The payoffs received by both scholars for every possible combination of moves.

\begin{figure}[htb]
\begin{center}
\includegraphics[width=85mm]{for-paper2.jpg}
\caption{SCG Binary Game Tree.}
\label{SCGextensive}
\end{center}
\end{figure}
%\includegraphics[scale=0.75]{scg-tree1.pdf}
%\includegraphics[height=1in,width=1in,angle=-90]{foo}
% \includegraphics{scg-tree1.pdf}


% The game tree is given by:
% 
% \begin{itemize}
% \item
% Proponent executes the action: propose claim {\it C} from {\it Claim}.
% \item
% Opponent: decide between 3 alternatives: 
% %\begin{itemize}
% %\item
% (1)
% {\it refute} (action refuteD({\it C})), 
% (2)
% %\item 
% {\it strengthen} (action strengthenD({\it C',C}) with 
% a stronger claim {\it C'} from {\it Claim}, i.e., \( stronger(C',C)), \) 
% (3)
% %\item 
% {\it agree} (action agreeD({\it C})).
% %\end{itemize}
% \end{itemize}
% Function {\it refute} directly invokes the refutation protocol\\ 
% \( {\it refute}(C,{\rm Proponent}, {\rm Opponent}).\)
% Function {\it strengthen} invokes the refutation protocol
% \({\it refute}(C',{\rm Opponent}, {\rm Proponent})\) with the scholars switched. 
% Function {\it agree} invokes the refutation protocol\\ 
% \({\it refute}(C,{\rm Opponent}, {\rm Proponent})\) also with the scholars switched.
% 

\subsubsection{Payoff function}
\label{payoff}
% The payoff information is determined by the refutation
% predicate \( p(c, ...) \). 
% The three dots \( ... \) refer to the data collected by the 
% refutation protocol, 
% consisting of a heterogeneous sequence of instances and solutions.
% The Proponent tries to make the refutation predicate true
% while the Opponent tries to make it false. The refutation is successful when the 
% predicate is false.
% 
Payoff is determined by:
(1) the decision of the opponent in the second move.
(2) the value of a refutation predicate which has as parameters the values collected 
along the current path back to the root. Including either the proposed claim $c$ or the 
strengthened claim $c'$, 
as well as instances $I$ and solutions $S$ provided during the refutation game.

We use the following notation to describe the payoff function:
$c.p(I, S)?{\rm (Pt, Ot),(Pf, Of)}$
If \(c.p(I, S)\) is true, {\rm Pt} is the payoff for the proponent and
{\rm Ot} is the payoff for the opponent.
If \(c.p(I, S)\) is false, Pf is the payoff for the proponent and
Of is the payoff for the opponent.

% We give an example of a payoff function, called 
% competitive payoff (zero-sum), which is the default pay-off function:

\begin{enumerate}
\item
If the opponent decision is {\it disputeD(c)}, the payoff is
$c.p(I,$ $S)$ $?$ $(1,$ $-1)$ $:$ $(-1,$ $1)$. The rationale is that if the predicate holds, the proponent has successfully supported $c$ and gets a 
point for that. The proponent failed to refute $c$ and loses a point. 
If the predicate is false, the opponent has failed to support $c$ and loses a point. The opponent has successfully refuted the $c$ and gets a point.
 

\item
If the opponent decision is {\it strengthenD(c, c')}, the payoff is
$c'.p(I,$ $S)$ $?$ $(-d,$ $d)$ $:$ $(1,$ $-1)$. where $d$ $=$ $c.distance(c,$ $c')$.
The rationale is that if the predicate holds, the opponent gets rewarded because she successfully supported her proposed stronger claim $c'$.
The payoff is proportional to the amount of strengthening as specified by the distance function to encourage more strengthening. 
If the predicate does not hold, the proponent has successfully refuted the stronger claim and gets rewarded with a point.
The strengthening was not successful.

\item
If the opponent decision is {\it agreeD(c)}, the payoff is
$c.p(I,$ $S)?$ $(0,$ $0)$ $:$ $(1,$ $-1)$.
The rationale is that if the predicate holds, the opponent has successfully supported the claim
and nobody gets a point because no dispute has taken place. Agreement is successful.
If the predicate does not hold, the opponent has failed to support the claim
and loses a point. Agreement is not successful.
\end{enumerate}


\subsection{Example}
Fig. \ref{SCGstructure} (top left) provides a summary of the {\it Domain}
structure. Fig. \ref{SCGstructure} (top right) provides an example of a {\it Domain}, the Gale-Shapley worst case domain. 
In this domain, {\it Instance} is the set of natural numbers, {\it Solution} is the set of preferences which is the input to
the Gale-Shapley matching algorithm. A solution {\it s} is valid for an instance {\it i} if and only if  {\it s} is syntactically well formed and
it gives preferences for {\it i} men and women. The quality of a solution {\it s} to an instance {\it i} is the number of iterations of
the while loop in the Gale-Shapley matching algorithm when supplied the preferences {\it s} as input.

Fig. \ref{SCGstructure} (middle left) provides a summary of the {\it Lab} structure and provides an example {\it Lab} (middle right), 
the Gale-Shapley worst case lab. {\it Claim}s in this lab have two parameters $n$ and $q$. $n$ is the number of men and women. $q$ is the number of
iterations of the Gale-Shapley matching algorithm that can be achieved by giving a preference for $n$ men and women. The instance set predicate 
of the claim selects only one instance, namely the instance where the number of men and women is the same as the claim parameter $n$. The refutation
protocol is that the opponent should provide an instance $I[0]$ satisfying the instance set predicate of the claim (there is only a singleton instance) and
the proponent should provide a preference $S[1]$ for $I[0]$. The refutation predicate holds if $S[1]$ causes the Gale-Shapley 
matching algorithm to iterate at least $q$ times. The $stronger$ predicate holds if the current claim has a higher value for the $q$ parameter. The distance
function $distance$ is defined as the difference between the $q$ parameter of the current and the given claim.
Several other examples in the style of Fig. \ref{SCGstructure} are in the supplementary materials \cite{SCGsupplementary}.

\begin{figure}[htb]
\begin{center}
\includegraphics[width=85mm]{SCGStructure.jpg}
\caption{SCG Structure.}
\label{SCGstructure}
\end{center}
\end{figure}



%\input{learning.tex}

%Depending on the application, many meaningful payoff functions can be defined.
%For example, if SCG is used for creating student interaction in
%a MOOC, I recommend the following low competition payoff function:
%
%\begin{enumerate}
%\item
%refute:
%\( p(c, ...)?(0,0):(0,1).\)
%If the predicate is true, nobody gets a point because we want the Opponent
%to learn from the Proponent through the refutation protocol.
%If the predicate is false, the Opponent has won and gets a point.
%
%\item
%strengthen c to c':
%\( p(c', ...)?(0,1):(0,0).\)
%If the predicate is true, the Opponent gets rewarded with one point because he 
%successfully defended the stronger claim.
%If the predicate is false, the Proponent has won but does not get a point
%because we want the Opponent to have cheap opportunities to attack and learn.
%
%\item
%agree:
%\( p(c, ...)?(0,1):(0,0).\)
%If the predicate is true, the Opponent has successfully defended the claim
%and nobody gets a point. 
%If the predicate is false, the Opponent has failed to defend the claim
%but has gained information to learn. The Proponent earns a point.
%\end{enumerate}
%The motivation is that it should be penalty free for students to learn
%from other students. Not succeeding in refuting a claim is free to the Opponent,
%while successfully refuting gives a point to the Opponent.
%Failing to strengthen a claim is free to the Opponent,
%while successfully strengthening gives a point to the Opponent.
%Failing to agree with a claim is free to the Opponent,
%while successfully agreeing gives a point to the Opponent
%This low competition payoff function has the flavor of a soccer game
%where only the goals count.
%
%The competitive payoff and the low competition payoff are two examples
%of payoff functions that promote good behavior in the lab.
%Other payoff functions are possible.
%
%Instances are only available when they are needed.
%For example, in the spirit of the Renaissance 
%mathematical competitions between Tartaglia and Fior, if the protocol asks that the
%Proponent  and Opponent deliver each 10 instances, followed
%by the solution activity.
%The instances are secret until they are solved.

% \subsection{Rules}
% 
% The rules for the SCG binary game are natural:
% follow the extensive-form representation of the game definition.
% A scholar loses immediately if he or she delivers an  element
% that is not in the specified set, 
% or if he or she does otherwise not follow the 
% refutation protocol.
% 
% All moves must be completed within the given resource (time, space, etc.) 
% limit.
% 
% The winner of a binary game is the scholar which achieves the highest payoff.
% The scholars are egoistic as they try to maximize their payoff.
% However, they will create social welfare
% (a knowledge base) when we engage them in a competition.

%\subsection{Game Histories}
%
%A game history for a binary game consists of a record like this:
%\begin{verbatim} 
%Claim: claimName(a,b,c); Quality: q; 
%Proponent: Alice; Opponent: Bob; 
%Agreement Refutation Protocol:
%  (provide | solve)* instances and solutions
%winner: Alice
%\end{verbatim} 

% \subsection{Extensions}
% 
% There are two easy extensions that are needed for more complex claims.
% (1) We might need multiple solve functions.
% For predicate calculus claims, the solve functions correspond to
% Skolem functions.
% (2) For multi-sorted domains, we need multiple Instance and Solution sets.
% Both changes require small extensions to the protocol language.
% Those changes do not influence the key game mechanisms.
% 
% Note that multiple solve functions can be avoided if we let the refutation
% predicate implement Skolem functions. The predicate returns not
% only the truth value, but also the result of calling
% the Skolem functions.

% done to here with grammarly

 \section{Beyond Binary SCG}
 \label{BeyoundBinarySCGSection}
 \subsection{Matches and Tournaments}
  To alleviate potential first-move-advantage in binary SCG, we propose that players
  engage in matches rather than binary games. A match consists of a number of rounds 
  of binary SCG where players switch the roles of opponent and proponent.
  Tournaments (e.g. round-robin, knock-out, Swiss-style) enable more than two players
  to engage in a single competition. Round-robin tournaments are more suitable for avatars
  playing SCG because they involve $n.(n-1)$ matches where $n$ is the number of players. Swiss-style
  tournaments are more suitable for humans playing SCG because it involves fewer games.
 
\subsection{Reputation Score}
 In real scientific communities, scientists build up their reputation based on their
 work and the breakthroughs they achieve. Likewise, in SCG, we propose to compute reputation scores, achieved in a particular lab, for 
 scholars based on their performance in competitions held in that lab as well as on their breakthroughs. 
%  The reputation of a scholar consists of two components:
% 	The payoff points collected and the breakthroughReputation points collected.

 \subsubsection{Breakthroughs}
Being the first in a scientific community is crucial for 
the reputation of a scholar. Therefore, the SCG as a 
faithful model of a scientific community,
also deals with being the first.

The breakthrough metric is computed after a 
competition or a series of competitions
as a retrospective.
For each important event, a time stamp is stored.
Important events are: refutation, support and strengthening.
We assume that we have the set of claims believed 
to be true ({\it BelievedTrue}) or false ({\it BelievedFalse}) or
optimal ({\it BelievedOptimal}).

For each claim in {\it BelievedTrue} or {\it BelievedOptimal},
we find the first scholar who proposed the claim
and supported it. That scholar gets one point added to the breakthrough component
of their reputation.

For each claim in {\it BelievedFalse},
we find the first scholar who successfully refuted the claim.
That scholar gets one point added to the breakthrough component
of their reputation.

For each claim in {\it BelievedTrue}, 
but not in {\it BelievedOptimal}, we find the first
scholar who successfully strengthened the claim and supported
the strengthened claim.
That scholar gets one point added to the breakthrough component
of their reputation.
%Encourages tiny strengthenings.

  
 \subsection{Histories and Open Publication}
 By publishing number of times a particular claim gets supported and refuted 
 and the reputations of players supporting or refuting these claims, 
 SCG creates social welfare.
 
 When a lab gets into a stable state (a sub-optimal equilibrium where breakthroughs 
 cease to happen for particular period of time),
it is time to publish the 
current, maybe imperfect refutation and support strategies.
If the scholars are avatars, their software is published.
If the scholars are humans, an informal description
of their techniques is published.

This levels the playing field and sets the stage 
for the next advancements. It is important to
reward the scholars for their previous investment
and not force them too early to publish their techniques.
 
  
  
\section{Discussion}
\label{DisscussionSection}

In this section we show how binary SCG can be seen from the perspective of current game design models.

\subsection{Five Element Game Ontology}
Using the 
five element game ontology by
Jose Zagal and Michael Mateas et al. \cite{Zagal05towardsan}:
interface, rules, goals, entities, and entity manipulation
we give an overview  of the SCG.
The {\bf entities} manipulated by the scholars are instances in {\it Instance},
solutions in {\it Solution} and claims in {\it Claim}
in the context of a {\it Lab} and
the reputation (payoff points) that a scholar accumulates.
The {\bf interface} for a scholar consists of the actions: 
{\it propose} a claim, decide to {\it refute}, {\it strengthen} or {\it agree} with a claim,
to {\it provide} an instance and to {\it solve} an instance.
The {\bf rules} of the SCG are the rules of the Scientific Method:
you must follow the refutation approach defined by {\it Lab}.
You also must follow the scientific discourse prescribed by the 
extensive form representation of the game.
The {\bf goal} of the game is to make the refutation protocol predicate
true or false, depending on the role you play (proponent or opponent of a claim).
The {\bf entity manipulation} includes solving instances with a certain
quality and creating claims and instances.
Gameplay is segmented into binary games and competitions and 
into increasingly more complex claims which become harder and harder to defend.

%We give an example of game segmentation that is in the domain of the
%Boolean Constraint Satisfaction Problem.
%Given a sequence $s$ of constraints,
%each expressed in terms of a relation from a set of Boolean relations $R$,
%find an assignment to the variables of $s$ that maximizes the fraction
%of satisfied constraints in $s.$
%The protocol asks for finding the maximum fraction \(0 \leq t(R) \leq 1 \)
%so that in any Boolean Constraint Satisfaction Problem
%using only relations in $R,$ the fraction $t(R)$
%can always be satisfied. 
%
%Natural levels for this scenario are
%(1) \( |R|=1,\)
%(2) \( |R|>1, \) the relations in \( R \) form an implication chain,
%(3) \( |R|>1, \) the relations in \( R \) form more than one implication chain.
%For defense strategies in this scenario, see \cite{lieber-specker:partial-2,jacm-81}.

\subsection{Triadic Game Design}
Using the model of Triadic Game Design \cite{triadic-book}
by Casper Harteveld,
we break down the SCG into a Reality, Meaning and Play component.
Triadic Game Design describes an approach to serious game design
and the SCG defines a large family of serious games.
The {\bf Reality} component of the SCG models a scientific community
based on the Popper-style Scientific Method \cite{nla.cat-vn1027910}.
The {\bf Meaning} component consists of cleaning the
knowledge base of false or non-optimal claims
by developing new constructions which are better
than the constructions of others.
The {\bf Play} component of the SCG consists
of competition, collaboration and finding a treasure (a new construction).


\subsection{Exploratory-Performatory Games}
According to Jonas Linderoth
\cite{exploratory-performatory} 
games challenge two aspects of human nature: our ability to choose appropriate actions and our ability to perform appropriate actions.
\cite{exploratory-performatory} views 
 gaming as a cycle between interrelated
 exploratory and performatory actions.

What are the exploratory and performatory actions in the SCG?
{\bf Exploratory} actions are: (1) proposing a claim which means choosing from a set of claims.
(2) Choosing an action: dispute, agree or strengthen a given claim.
{\bf Performatory} actions are: (1) the proponent should defend the proposed claim.
(2) If an opponent decides to refute, he should succeed in refuting, etc.
In the SCG we also have a cycle of interrelated exploratory and performatory actions.
Indeed, this cycle is the dominant activity in the SCG.



  
% \section{}
% 
% Domain  															GaleShapleyWorstCaseDomain
%    Instance																Nat
%    Solution																Preferences
%    valid(i : Instance, s : Solution) : Boolean							valid(i Nat, s) = s is syntactically correct
%    quality(i : Instance, s : Solution) : Real							quality(i, s) = GS iterations for s and i
%   	 
% Lab																	GaleShapleyWorstCaseLab
% 	Domain																GaleShapleyWorstCaseDomain
% 	proto : Protocol														O:I[0], P:S[1] of I[0]
% 	Claim																GaleShapleyWorstCaseClaim
% 																			n : Nat
% 																			q : Nat
% 		isp(i : Domain.Instance) : Boolean									isp(i) = (i == n)
% 		p(I : Domain.Instance[], S : Domain.Solution[]) : Boolean			p(I, S) = Domain.quality(I[0], S[1]) >= q
% 		stronger(c : Claim) : Boolean										stronger(c) = q > c.q			
% 		distance(c : Claim) : Real											distance(c) = q - c.q
%    
%    
% A Domain type consists of an Instance type and a solution type   
% 
%   

\section{Binary SCG Analysis}
\label{propertiesSection}
  In this section, we characterize blameable moves in the binary SCG game tree. We argue that blame is both fair and is consistent with the design goal of 
  encouraging scholars to put as much effort and intelligence as possible into proposing claims that are hard to falsify as well as into 
  attempting to refute those claims. We show that the payoff is sound, fair, and competitive with respect to the blame assignment. These three properties
  are important for SCG to be interesting. For space reasons, we deal in this subsection only with bivalent labs.
  
\subsection{Blame Assignment}
  First, we divide the branches of the SCG game tree into 8 different sets based on 3 properties. Then, we assign blame to these sets.
  Figure~\ref{SCGCSPTable} presents these sets.
  The three properties are: (1) whether the proponent proposed a true claim or not. This is represented in Figure~\ref{SCGCSPTable} by the column {\bf claim}.
  A value of {\tt T} means the proposed claim is true. A value of {\tt F} means the proposed claim was false.
  (2) the decision made by the opponent. This is represented in Figure~\ref{SCGCSPTable} by the column {\bf dec}. 
  A value of {\tt a} means agree and a value of {\tt d} means dispute. There is no strengthening in bivalent labs.
  (3) the outcome of the refutation game and the winner. This is represented in Figure~\ref{SCGCSPTable} by the column {\bf out}. The outcome is either {\tt s} for ``support" or {\tt r}
  for ``refutation'' and the winner is either {\tt P} for the ``proponent'' or {\tt O} for the ``opponent''.
  
  Figure~\ref{SCGCSPTable} has two blame columns {\bf cB}, and {\bf oB} with values that are either 
  {\tt P} for the ``proponent'' or {\tt O} for the ``opponent''. In the {\bf cB} column, we blame the proponent for
  proposing a false claim (rows 1, 3, 5, 7). This is consistent with our design goal of encouraging scholars to put effort and intelligence 
  into proposing claims that are hard to falsify. This blame is fair because it is in the hands of the proponent to avoid. 
  %Regardless of the move taken by the opponent, both the proponent and the opponent participate into a refutation game. This is consistent with the design goal of encouraging refutation attempts.
  In the {\bf oB} column, we blame the player that has lost the refutation game when it is fair to do so. This is consistent with our design
  goal of scholars to put effort and intelligence into attempting to refute claims. The blame in this column is fair because it is in the hands of
  both players to avoid. The opponent gets blamed for failing to refute a claim it disputed (rows 3, 4) and for failing to support a claim it agreed with (rows 5, 6).
  The proponent gets blamed for failing to support a claim it proposed (rows 7, 8). The proponent does not get blamed for failing to refute a claim it proposed (rows 1, 2).
  
  
% The definition of those properties depends on the
% SCG CSP Table
% (see Figure \ref{SCGCSPTable} with the competitive payoff function).
% which analyses the SCG game tree
% (see Figure \ref{SCGextensive} on page \pageref{SCGextensive} with the competitive payoff function).
% The SCG CSP Table has 8 rows based on the 3 independent
% variables: 
% {\bf claim} (true/false) abbreviated (T/F), 
% {\bf dec} (dispute/agree) decision abbreviated (d/a) and
% {\bf out} (refuted/supported) outcome abbreviated (r/s).
% The claim variable value we would like to determine
% by playing the game. The dec (decision) variable is assigned 
% by the second game decision. The out (outcome) variable is assigned
% by the refutation game where the claim is either
% refuted or supported.
% For the outcome we also list the winner of the game:
% sO means the claim was supported and the winner is O.
% 
% The SCG CSP Table has besides
% the three independent variables claim, action and outcome,
% three dependent blame variables {\bf cP}, {\bf aB} and {\bf oB} with
% values P (proponent) or O (Opponent).
% Blame is is assigned as shown in the Blame Justification
% column of the SCG CSP Table.
% The blame justification (last column) is for the oB column only
% and the justification is independent of whether
% the claim is true or false. The justification is based on
% the observable variables dec and out.
% The justification for the cB column is:
% Proposing a false claim leads to a blame for P in column cB.
% For the decision blame column aB,
% agreeing with a false claim or disputing a true claim 
% leads to a blame for O. 

\subsection{Payoff Function}
In the design of the SCG payoff function there 
are three forces at work that need to be balanced.
We would like the payoff function to be fair, sound
and competitive.
\subsubsection{Incomplete Knowledge and Fairness}
 Unfortunately, it is not always decidable whether a claim is true or false. Therefore, the payoff has to be
 the same for branches (rows of Figure~\ref{SCGCSPTable}) that only differ in the {\bf claim} property (namely, rows \{1, 2\}, \{3, 4\}, \{5, 6\} and \{7, 8\}). 
 For the payoff to be fair, it has to give scholars the benefit of the doubt (i.e. the payoff function has to only penalize a scholar for a group of 
 rows where the scholar is blamed in every row of the group). For example, 
 it is unfair to blame either the proponent or the opponent for rows \{1, 2\} because none of the players are blamed in row 2. 
 The payoff function shown in Figure~\ref{SCGCSPTable} is fair.
 
\subsubsection{Soundness}
  For the payoff to be sound, there must be a chance that a scholar gets eventually penalized if it makes a blameable move. 
  For example, suppose that the proponent proposed a false claim. There are 4 possible branches that start with the proponent proposing a false claim, 
  and they correspond to rows 1, 3, 5, 7 in Figure~\ref{SCGCSPTable}. To be sound, the payoff function must penalize the proponent in one of these rows.
  The payoff function shown in Figure~\ref{SCGCSPTable} penalizes the proponent in row 7. The payoff function shown in Figure~\ref{SCGCSPTable} is sound.
  
\subsubsection{Competitiveness}
  For the payoff to be competitive, it must encourage competition until the last move (i.e. the last move must matter to the payoff). In our case, the last 
  move consists of playing the refutation game. The payoff function must encourage scholars to win the refutation game. For example,
  the payoff function should favor the proponent in row 5 more than it does in row 1. Because, both rows only differ in the refutation game winner
  which is the proponent for row 5 and the opponent for row 1. The payoff function shown in Figure~\ref{SCGCSPTable} is competitive.
  
  
% %\subsection{Fairness and Soundness of Payoff}
% 
% % For space reasons, we deal in this subsection only with
% % bivalent labs
% % (all claims are either true or false) without optimization. 
% 
% In the design of the SCG payoff function there 
% are three forces at work that need to be balanced.
% We would like the game to be fair, sound
% and competitive.
% The definition of those properties depends on the
% SCG CSP Table
% (see Figure \ref{SCGCSPTable} with the competitive payoff function).
% which analyses the SCG game tree
% (see Figure \ref{SCGextensive} on page \pageref{SCGextensive} with the competitive payoff function).
% The SCG CSP Table has 8 rows based on the 3 independent
% variables: 
% {\bf claim} (true/false) abbreviated (T/F), 
% {\bf dec} (dispute/agree) decision abbreviated (d/a) and
% {\bf out} (refuted/supported) outcome abbreviated (r/s).
% The claim variable value we would like to determine
% by playing the game. The dec (decision) variable is assigned 
% by the second game decision. The out (outcome) variable is assigned
% by the refutation game where the claim is either
% refuted or supported.
% For the outcome we also list the winner of the game:
% sO means the claim was supported and the winner is O.
% 
% The SCG CSP Table has besides
% the three independent variables claim, action and outcome,
% three dependent blame variables {\bf cP}, {\bf aB} and {\bf oB} with
% values P (proponent) or O (Opponent).
% Blame is is assigned as shown in the Blame Justification
% column of the SCG CSP Table.
% The blame justification (last column) is for the oB column only
% and the justification is independent of whether
% the claim is true or false. The justification is based on
% the observable variables dec and out.
% The justification for the cB column is:
% Proposing a false claim leads to a blame for P in column cB.
% For the decision blame column aB,
% agreeing with a false claim or disputing a true claim 
% leads to a blame for O. 
% %For the outcome column oB:
% %(1)
% %P gets blamed if P fails to force the refutation of
% %a false claim or if P fails to defend a true claim;
% %(2)
% %O gets blamed if O fails to refute a false claim or
% %if O failed to refute a claim it disputed.
% 
% %The column {\bf np} is about {\bf not perfect} players.
% %A player P is not perfect if O supports a false claim against P
% %or
% %O refutes a true claim against P.
% 
% %\begin{figure}[htb]
% %\begin{center}
% %\includegraphics[width=95mm]{SCG-Blame-Table2.jpg}
% %\caption{SCG Blame Table.}
% %\label{SCGBlameTable}
% %\end{center}
% %\end{figure}
% Finally, the {\bf P} and {\bf O} columns give the payoff values
% for the proponent P and opponent O. Notice that the 
% payoff function has identical values for row pairs
% (1,2) and (3,4) and (5,6) and (7,8).
% 
% A game is {\bf fair} if for all rows the following property holds: 
% If P (or O) lose a point they are blamed in that row.
% See Figure \ref{SCGCSPTable} for an example of a fair
% game.
% 
% Note that if P could have made a mistake, but we are not sure because
% we don't know whether the claim is true or false, we don't punish P.
% Therefore, if P made a point, it could still be blamed.
% We give P the benefit of the doubt.

% The soundness definition has two parts:
% Definitive soundness and chance soundness.
% The first kind of soundness is about the oB column:
% if you get blamed for losing a refutation game you 
% will have a negative payoff.
% The second kind of soundness is about the cB and aB
% columns: if you get blamed in those columns you 
% take the risk of having a negative payoff.
% It depends on your opponent whether she will
% expose the reason for the blame.
% 
% A game is {\bf oB-sound} if for all rows the
% following property holds:
% if P (or O) are blamed in the oB column, they have a negative payoff in that row.
% The game in
% Figure \ref{SCGCSPTable} is oB-sound.
% 
% A game is {\bf cB-sound} if there exists a row
% in which P is blamed in the cB column and there is a negative payoff for P.
% The game in
% Figure \ref{SCGCSPTable} is cB-sound.
% Proof: If P is blamed in column cB, the optimal response for 
% O is to dispute the claim and then to refute it.
% Row 7 has a negative payoff for P.
% 
% Informally, cb-sound means that if you get blamed in the cB column
% you risk of being punished by a strong opponent.
% 
% %A game is {\bf cB-sound} if for all rows the
% %following property holds:
% %if P is blamed in the cB column, there is a chance
% %that P will have a negative payoff if O plays better.
% %The game in
% %Figure \ref{SCGCSPTable} is cB-sound.
% %Proof: If P is blamed in column cB, the optimal response for
% %O is to dispute the claim and then to refute it (row 7).
% 
% %A game is {\bf aB-sound} if for all rows the
% %following property holds:
% %if O is blamed in the aB column, there is a chance
% %that O will have a negative payoff if O plays better.
% 
% A game is {\bf aB-sound} if for all rows where O is blamed in the aB column,
% there is a chance
% that O will have a negative payoff if P plays better.
% The game in
% Figure \ref{SCGCSPTable} is aB-sound.
% The proof involves two cases.
% The first case is: O makes the mistake of agreeing with a false claim (F a, row 1 and row 5).
% We search for a row with the same prefix (F a) where P is the winner.
% We find row 5 where the payoff is indeed negative for O.
% The second case is: O makes the mistake of disputing a true claim (T d, row 4 and row 8).
% We search for a row with the same prefix (T d) where P is the winner.
% We find row 4 where the payoff is indeed negative for O.
% 
% 
% A game is {\bf sound} if it has all three properties:
% oB-sound and 
% cB-sound and
% aB-sound.
% 
% 
% %{\bf Do case analysis}
% 
% %For the weakly soundness definition we assume that
% %all scholars are perfect duriing the refutation game.
% %This restriction eliminates the starred rows
% %from the table.
% %A game is {\bf weakly sound} if for all remaining 4 rows
% %the following property holds:
% %if P (or O) are blamed they have a negative payoff in that row.
% %The game in
% %Figure \ref{SCGCSPTable} is not weakly sound
% %because of row 5.
% %In row 5, P is blamed but has a positive payoff (1).
% %
% %We can make the game in Figure \ref{SCGBlameTable} weakly sound
% %by changing the payoff on rows 5 an 6 from 1,-1 to -1,-1.
% %But then the game is no longer fair because on row 6,
% %P has a negative payoff but is not blamed.
% 
% The third important game property is competitiveness.
% A game is {\bf competitive} if it matters whether you 
% win or lose: the payoff value is higher for the winner.
% The game in
% Figure \ref{SCGCSPTable} is competitive.
% %Comparing rows 1 and 5, in row 1 the opponent wins and makes
% %0 points while in row 5 the opponent makes -1 points
% %because the opponent loses.
% %Similarly for rows 2 and 6.
% %Comparing rows 3 and 7, in row 3 the proponent wins and makes
% %one opponent while in row 7 the proponent makes -1 points.
% %A similar argument holds for rows 4 and 8.
% 
% {\bf Theorem: Good Payoff}
% There exists a payoff function which has all three
% properties:
% fair, sound and competitive.
% 
% Proof:
% The game in Figure \ref{SCGCSPTable} is fair,
% competititive and sound.
% 
%\input{weak-soundness}

\begin{figure}[htb]
\begin{center}
\includegraphics[width=85mm]{SCG-CSP.jpg}
\caption{Blame and Payoff Table}
\label{SCGCSPTable}
\end{center}
\end{figure}

\subsection{Payoff Function Design using CSP}
To study the space of payoff functions, we introduce
a constraint satisfaction problem that expresses
the constraints implied by the fairness, soundness and competitiveness
properties.
Figure \ref{SCGCSPTable} introduces eight variables for
formulating the constraints for the payoff function:
$paso$, $oaso$, etc. The variable names come from the decision and outcome column.

To penalize the proponent we add the constraint that its payoff must be negative.
We say that the difference between the proponent and opponent payoffs is the amount that the payoff function favors the proponent with.

The constraints for the fairness property are: 
\( paso \geq 0,\) and
\(oaso \geq 0,\) and
\(pdsp \geq 0,\) and
\(parp \geq 0,\) and
\(odro \geq 0.\). 


The constraints for soundness we give separately for oB-soundness (soundness based on blame in the oB column) and cB-soundness (soundness based on blame in the cB column).
The constraints for the oB-soundness property are: 
\( odsp < 0,\) and
\( oarp < 0,\) and
\( pdro < 0.\).

For cB-soundness, there is one constraint which is: 
\( ((pdro < 0) \vee (parp<0) \vee (pdsp<0) \vee (paso<0)).\) 
%because row 7 must have a negative
%payoff for P. It is on line 7 where the false claim gets disputed and refuted.

% For aB-sound the first constraint  is \(((oaso<0) \vee (oarp < 0))\) because row
% 1 or 5 must have a negative
% payoff for O.
% The second constraint  is \( ((odsp < 0) \vee (odro<0)) \) because row 4 or 8 must have a negative
% payoff for O.

The constraints for competitiveness are:
\(parp-oarp > paso-oaso\) and \(pdsp-odsp > pdro-odro.\)
% The rationale is as follows: 
% In case of agreement, the difference between the payoff of the proponent 
% and the payoff of the opponent when the proponent wins \((parp-oarp),\) is larger 
% than the corresponding difference when the opponent wins \( (paso-oaso).\)
% Therefore, wining the refutation game is advisable for both parties.
% The second constraint applies for the case of dispute.
% 

Any variations of the payoff function must satisfy all constraints introduced above
for the game to be fair, sound and competitive. The above constraints 
are also useful when only a subset of the properties is desired.


\section{Experience with the SCG}
\label{ExperienceSection}
The SCG has evolved since 2007. We have used the SCG in
software development courses at both the undergraduate
and graduate level and in several algorithm courses.
Detailed information about those courses is available from
the second author's teaching page.

\subsection{Software Development}
The most successful graduate classes
were the ones that developed and maintained the
software for SCG Court
\cite{SCGCourt}
as well as several labs and their avatars to test SCG Court. 
Developing labs for avatars has the flavor of 
defining a virtual world for artificial creatures.
At the same time, the students got detailed
knowledge of some problem domain and how to solve it.
A fun lab was the Highest Safe Rung lab from
\cite{Kleinberg:1051910} where the best avatars needed
to solve a constrained search problem using
a modified Pascal triangle.

\subsection{Algorithms}
The most successful course 
(using \cite{Kleinberg:1051910} as textbook)
was in Spring 2012 where
the interaction through
the SCG encouraged the students to solve difficult problems.
Almost all homework problems were defined through labs
and the students posted both their exploratory and performatory
actions on piazza.com.
We used a multiplayer version of the SCG binary game
which created a bit of an information overload.
Sticking to binary games would have been better
but requires splitting the students into pairs.
The informal use of the SCG through Piazza (piazza.com) 
proved successful. All actions were expressed in JSON
which allowed the students to use a wide variety
of programming languages to implement their algorithms.

The students collaboratively solved several problems
such as the problem
of finding the worst-case inputs for the Gale-Shapley algorithm
(see the section Example above).

We do not believe that, without the SCG, the students would
have created the same impressive results. The SCG effectively
focuses the scientific discourse on the problem
to be solved.

The SCG proved to be adaptive to the skills of the students.
A few good students in a class become effective
teachers for the rest thanks to the SCG mechanism.

%\section{Scientific Community}
%
%The informal model behind our scientific communities
%is described by the following list.
%Scholars are encouraged to
%(1) propose claims that are not easily improved.
%(2) Propose claims that they can successfully defend.
%(3) Quote related claims  and show how they improve on previous claims.
%(4) Prove claims if the current state of the art allows.
%(5) Stay active and propose new claims or oppose current claims.
%(6) Be well-rounded: solve posed instances
%and pose difficult instances for others.
%(7) Become famous! (maximizing their payoff and be the first
%to propose and defend a true or optimal claim).
%

\section{Related Work}
\label{RelatedSection}
The SCG has not grown in a vacuum. We make connections to several related areas.

\subsection{Crowd Sourcing and Human Computation}

There are several websites that organize competitions.
What is common to many of those competitions? We believe that 
the SCG provides a foundation to websites such as
TopCoder.com
%TopCoder \cite{TopCoder} 
or kaggle.com.
%which is more specialized.

The SCG makes a specific, but incomplete proposal of a programming interface to
work with the global brain
\cite{Bernstein:2012:PGB:2160718.2160731}.
What is currently missing is a payment mechanism for 
scholars and an algorithm to split workers into
pairs based on their background.

The SCG is a generic version of the ``Beat the Machine'' approach
for improving the performance of machine learning systems
\cite{attenberg2011beat-ipeirotis}.

Scientific discovery games, such as FoldIt and EteRNA,
are variants
of the SCG.
\cite{Cooper:2010:CDS:1822348.1822354} describes the
challenges behind developing scientific discovery games.
\cite{Andersen:2012:ITG:2207676.2207687} argues that complex
games such as FoldIt benefit from tutorials.
This also applies to the SCG,
but a big part of the tutorial is reusable
across scientific disciplines.

\subsection{Logic and Imperfect Information Games}
Logic has long promoted the view
that finding a proof for a claim is the same as finding a defense strategy
for a claim.


Logical Games
\cite{LogicalGames}, 
\cite{sep-logic-games}
have a long history going back to Socrates.
The SCG is an imperfect information game which builds on 
Paul Lorenzen's dialogical games \cite{sep-logic-dialogical}.

\subsection{Foundations of Digital Games}

%According to Jonas Linderoth
%\cite{exploratory-performatory} 
%games challenge two aspects of human nature: our ability to choose appropriate actions and our ability to perform appropriate actions.
%\cite{exploratory-performatory} views 
% gaming as a cycle between interrelated
% exploratory and performatory actions.
%
%What are the exploratory and performatory actions in SCG?
%Exploratory actions are: (1) proposing a claim which means choosing from a set of claims.
%(2) Choosing an action: refute, agree or strengthen a given claim.
%Performatory actions are: (1) the proponent should defend the proposed claim.
%(2) If an opponent decides to refute, he should succeed in refuting, etc.
%In SCG we also have a cycle of interrelated exploratory and performatory actions.

A functioning game should be deep, fair and interesting which requires careful
and time-consuming balancing.
\cite{AIIDE125470} describes techniques used for balancing that complement
the expensive playtesting. This research is relevant
to SCG lab design. For example, if there is an easy way to refute claims
without doing the hard work, the lab is unbalanced.
%SCG has the interesting property that 
%if a ``clever procedure'' is known
%to scholar Alice but, not to scholar Bob, Alice can easily win over Bob.
%If both know the clever procedure, the game is a tie.
%The goal of an SCG lab is to discover such a clever procedure.

\subsection{Architecting Socio-Technical Ecosystems}

This area has been studied by James Herbsleb and the
Center on Architecting Socio-Technical Ecosystems (COASTE) at CMU
http://www.coaste.org/.
A socio-technical ecosystem supports straightforward
integration of contributions from many participants
and allows easy configuration.

The SCG has this property and provides a specific 
architecture for building knowledge bases in
(formal) sciences. 
Collaboration between scholars is achieved through
the scientific discourse which exchanges instances
and solutions. The structure of those instances and solutions
gives hints about the solution approach. An interesting
question is why this indirect communication approach
works.
% so well.

The NSF workshop report \cite{ScacchiNSFReport} discusses socio-technical innovation
through future games and virtual worlds.
The SCG is mentioned as an approach to make the scientific method 
in the spirit of Karl Popper available to CGVW (Computer Games and Virtual Worlds).

\subsection{Online Judges}

An online judge is an online system to test programs in programming contests.
A recent entry is \cite{Petit:2012:JEP:2157136.2157267} where private inputs
are used to test the programs. 
%\cite{TopCoder} 
Topcoder.com includes an
online  judge capability, but where the inputs are provided by competitors. 
This dynamic benchmark capability is also expressible with the SCG: 
The claims say that for a given program, all inputs
create the correct output. A refutation is an input which
creates the wrong result.

\subsection{Educational Games}
The SCG can be used as an educational game. One way to create adaptivity for learning
is to create an avatar that gradually poses harder claims and instances.
Another way  is to pair the learner with another learner who is stronger.
\cite{Andersen:2012:OAE:2282338.2282398} uses concept maps to guide the learning.
Concept maps are important during lab design: they describe the concepts that need
to be mastered by the students for succeeding in the game.

\subsection{Formal Sciences and Karl Popper}
James Franklin points out in
\cite{Franklin1994-FRATFS}
that there are also experiments in the formal sciences. One of them is the `numerical
experiment' which is used when the mathematical model is hard to solve.
For example, the Riemann Hypothesis and other conjectures have resisted proof
and are studied by collecting numerical evidence by computer.
In the SCG experiments are performed when the refutation protocol is elaborated.

Karl Popper's work on falsification
\cite{nla.cat-vn1027910}
is the father of non-deductive methods in science.
The SCG is a way of doing science on the web according to Karl Popper.

\subsection{Scientific Method in CS}

Peter Denning defines CS as the science of information processes
and their interactions with the world \cite{Denning:2005:CSS:1053291.1053309}.
The SCG makes the scientific method easily accessible by expressing the
hypotheses as claims.
Robert Sedgewick in \cite{ScientificMethodProgramming} stresses the importance of
the scientific method in understanding program behavior.
With the SCG, we can define labs that explore the fastest
practical algorithms for a specific algorithmic problem.

\subsection{Games and Learning}
Kevin Zollman studies the proper arrangement of communities of learners
in his dissertation on network epistemology \cite{Zollman2007-ZOLTCS}.
He studies the effect of social structure on the reliability
of learners.

In the study of learning and games the focus has been on learning
known, but hidden facts.
The SCG is about learning unknown facts, namely new constructions.

\subsection{CSP-based Game Design}
CSP is increasingly being used in the procedural content generation (PCG) community, although not in industry.
For example,
Tanagra\cite{Smith:2010:TML:1822348.1822376} uses a numerical constraint 
solver to guarantee level playability.
In addition, Magy El-Nasr
used constraint solving for lighting and adaptive systems for games
\cite{El-Nasr:2004:ALD:1008213.1008238}.


\subsection{Origins of SCG}

A preliminary definition of the SCG was given in a keynote paper
\cite{scg-bionetics}.
\cite{scghome} gives further information on the \SCGp.
The original motivation for the SCG came from the two papers with Ernst Specker:
\cite{jacm-81} and the follow-on paper
\cite{lieber-specker:partial-2}.
Renaissance competitions are another motivation: the public problem solving duel between Fior and
Tartaglia, about 1535, can easily be expressed with the SCG protocol language.

\section{Future Work}
\label{FutureWorkSection}
We see a significant potential in putting the refutation-based Scientific Method 
into the cyberinfrastructure and make it widely available.
We plan to, iteratively, improve our current implementation
based on user feedback.

We see an interesting opportunity to mine the game histories and make suggestions
to the scholars how to improve their skills to propose and defend claims.
If this approach is successful, the SCG will make contributions to computer-assisted 
problem solving.

\section{Summary and Conclusions}
\label{ConclusionSection}
The SCG provides a simple interface to 
a community that uses the (Popperian) Scientific Method.
The SCG provides for effective
customization of the generic scientific machinery 
by using lab definitions. Since the SCG models
a scientific community it is a broad enabling tool for innovation and learning
%widely applicable
and deserves a central place in the world's cyberinfrastructure
and serious games world.
We believe that the game design approach we outline in this paper
has many applications to other games.
We start with a game goal and translate
it into a blame assignment for moves 
that are inconsistent with the design goal.
Then we derive a payoff function
that is fair, sound and competitive.
Such a systematic approach eliminates a lot of game testing because
we know that many properties are formally guaranteed.

{\bf Acknowledgments:} We would like to thank 
% Ahmed Abdelmeged,
Bryan Chadwick, Magy Seif El-Nasr, David Lazer, Rory Smead,
Abraham Bernstein and Gillian Smith for their input and
feedback on the paper.


%\section{Future Work}

%There is one aspect missing in SCG: timing. In science the first
%proponent and defender of an idea gets special credit. Also those scholars
%who provide stepping stones for others get credit (citation counts).

%Proposal:
%Use timestamps for all proposals, refutations, defenses and strengthenings.
%Do a retrospective of a competition or a series of competitions.
%
%Compute first times:
%
%First time a claim is proposed, refuted, defended or strengthened.
%
%Reward first scholar if the refuted claim is false.
%
%Reward first scholar if the proposed or defended or strengthened claim is true or optimal. 
%
%
%true, false, optimal may have uncertainty: true = mostly defended.
%false = mostly refuted.
