\documentclass{sig-alternate}
\usepackage{times}
\usepackage{url}
\usepackage{graphics}
\usepackage{color}
\usepackage{xspace}
\usepackage{listings}
\usepackage[pdftex]{hyperref}
\hypersetup{%
pdftitle={SCG},
pdfauthor={Your Authors},
pdfkeywords={your keywords},
bookmarksnumbered,
pdfstartview={FitH},
colorlinks,
citecolor=black,
filecolor=black,
linkcolor=black,
urlcolor=black,
breaklinks=true,
}
\newcommand{\comment}[1]{}
\newcommand\gap{\;\;}

\definecolor{Orange}{rgb}{1,0.5,0}
\newcommand{\todo}[1]{\textsf{\textbf{\textcolor{Orange}{[[#1]]}}}}


\newcommand{\period}[1]{#1\xspace}
\newcommand\SCG{\period{Scientific Community Game}}
\newcommand\SCGp{Scientific Community Game}

% from bionetics
\newcommand\demj{DemeterJ}
\newcommand\sgdp{SCG Design Pattern}
%\newcommand\sgdp{Systematic Game Design Pattern}

% for this paper
\newcommand\OmegaA{$\Omega\mbox{-}structure ~ \mathcal{A}$}
\newcommand\Omegaphi{ $\Omega\mbox{-}formula ~ \phi$}

\DeclareFontFamily{\encodingdefault}{\ttdefault}{\hyphenchar \font=-1}
\newcommand{\code}[1]{\texttt{#1}}

\pagenumbering{arabic}  % Arabic page numbers for submission.  Remove this line to eliminate page numbers for the camera ready copy

\begin{document}
% to make various LaTeX processors do the right thing with page size
\special{papersize=8.5in,11in}
\setlength{\paperheight}{11in}
\setlength{\paperwidth}{8.5in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

% use this command to override the default ACM copyright statement 
% (e.g. for preprints). Remove for camera ready copy.
\toappear{To be submitted for review to the ACM Web Science 2013 Conference in Paris, May 2-4. 10 pages limit. Due Feb. 1, 2013}

\title{
FSCP: A Platform for Crowdsourcing Formal Science
%Crowdsourcing for STEM Knowledge Bases and The Know-How To Defend Them OR 
%Social Software for Computational Communities
%
% The Scientific Community Game:\\
% A Crowdsourcing Platform for Scientific Innovation \\
% Using Unreliable Scientists
%
%A Lens to Focus the Global Brain
%A Sociotechnical Architecture for Problem Solving
}
\numberofauthors{2}
\author{
  \alignauthor Ahmed Abdelmeged\\
    \affaddr{Northeastern University}\\
    \email{mohsen@ccs.neu.com}
  \alignauthor Karl Lieberherr\\
    \affaddr{Northeastern University}\\
    \email{lieber@ccs.neu.edu}
}

\maketitle
\begin{abstract}
We present the Formal Science Crowdsourcing Platform (FSCP).
FSCP represents claims as interpreted predicate logic formulas.
FSCP-based crowdsourcing systems focus a crowd of scholars on examining 
a family of claims to separate the true claims from false ones. 
Scholars examine a claim through participating in a substantiation game.
Substantiation games are built on top of Hintikka's Game Theoretical 
Semantics (GTS). Furthermore, FSCP collects the defense and attack 
strategies on claims.

We also present an approach to evaluate scholars that we believe is new.
We also present two approaches to estimate the truth likelihood of claims.
We report on our experience with using an earlier version of FSCP in class.
% 
%  build knowledge bases
% of predicate logic formulas 
% Crowdsourcing contests have received a lot of attention
% in recent years. We study the general problem how to
% use crowdsourcing to build knowledge bases and to collect the
% know-how
% to defend the claims in the knowledge base.
% We express claims in a knowledge base as predicate logic formulas.
% To challenge the crowd and discourage weak participants,
% all assertions of the form: "This claim is true"
% must be substantiated by one or more games to be won.
% All these substantiation games are refutation games associated
% with the formula of the claim.
% 
% We define a generator of crowdsourcing systems which is paramaterized
% by labs that focus the crowd on a specific task.
% We mention key properties of our system and we report
% on our experience in using the approach in teaching.
% 
\end{abstract}

\keywords{
Crowdsourcing, Human computation, STEM innovation and education,
epistemology, dialogic games, Karl Popper, mechanism design,
social welfare, logic, defense strategies, games and quantifiers, virtual communities.
} 


%\category{H.5.2}{Information Interfaces and Presentation}{Miscellaneous}[Optional sub-category]
%

\section{Introduction}
\label{sec:introduction}
Crowdsourcing contests have received a lot of attention in recent years. 
A crowdsourcing system is a generic system that enlists a crowd of users to help solve a problem 
defined by the system owners~\cite{CrowdsourcingSystemsOnTheWWW}. 

% To build a successful crowdsourcing 
% systems, one must face four challenges: how to recruit and retain users; what contributions can users make;
% how to combine user contributions to solve the target problem; and how to evaluate them~\cite{CrowdsourcingSystemsOnTheWWW}.

This paper presents the Formal Science Crowdsourcing Platform (FSCP), a highly configurable platform for constructing
crowdsourcing systems for formal scientific knowledge. FSCP represents formal scientific knowledge as a set of claims. A claim is a 
predicate logic formula where all nonlogical symbols (i.e. constants, functions and predicates) are interpreted in a particular domain. 
Logical connectives are interpreted using the Game Theoretic Semantics (GTS) of Hintikka to yield two-person, zero-sum games, called refutation games (a.k.a semantical games). 
The two players are called the verifier and the falsifier. The existence of a winning strategy for the verifier means that the formula is true, 
the existence of a winning strategy for the falsifier means that the game is false.

In FSCP, owners specialize the platform by creating labs. 
A lab is a crowdsourcing system that focuses a crowd of scholars on examining 
a family of claims to separate the true claims from false ones. 
Claim families are constructed by partially interpreting nonlogical symbols of a predicate logic formulas in a particular domain.   
Individual claims are obtained by completing
the interpretation in the same domain. Scholars contribute to the lab by participating in refutation games that are syntactically derived from claims. By doing so, 
scholars provide evidence to the truth likelihood of individual claims in the lab. Furthermore, playing those games helps building the knowledge and intuition
of individual scholars regarding the critical constructions of examples and counter examples embedded in the current winning strategies. The FSCP evaluates 
the performance of individual scholars as well as the truth likelihood of individual claims based on the history of all refutation games played in a 
particular lab. 


\subsection{FSCP Applications}
FSCP 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 FSCP 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 FSCP 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 FSCP 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{Organization}
This paper is organized as follows: In section~\ref{sec:platform} we present FSCP while 
in section~\ref{sec:scholar:evaluation} we present a novel approach for evaluating scholars and an approach for computing the truth likelihood of claims.
In section~\ref{ExperienceSection}, we present our experience with SCG, a very close predecessor of FSCP.
In section~\ref{RelatedSection}, we present some of the related work. 
Section~\ref{sec:conc:fw} concludes the paper.


% FSCP can be seed as adopting the model of science proposed by Karl Popper, the prominant science philosopher of the 20th century. 
% In his book, ``Conjectures and Refutations'', Popper promoted the ideas 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. 
% 
% 
% 
% The Scientific Community Game (SCG) is a crowdsourcing platform for science. SCG adopts model of science 
% proposed by Karl Popper, the prominant science philosopher of the 20th century. In his book, 
% ``Conjectures and Refutations'', Popper promoted the ideas 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 SCG to encourage scholars to put as much effort and intelligence as possible into 
% \emph{proposing claims that are hard to falsify} as well as into \emph{attempting to refute those claims}.
% Eventually, we mine the history of interactions taking place as a part of the game play to
% \emph{identify the correctness likelihood of claims}, among other things. 
% SCG tries recruit and retain users through a game mechanism that we strive to make it meaningful, 
% sound, intrinsically rewarding and competition encouraging. 
% SCG focuses the crowd on a particular family of claims. Finally, we designed SCG to be highly configurable
% with respect to claims as well as game mechanisms so that it fits a wide range of applications.
% 
% \subsection{SCG in a Nutshell}
% Lab designers are a particular class of platform users that specialize SCG through creating labs. A lab
% defines a family of claims as well as a particular game mechanism to be used. A lab is effectively a crowdsourcing 
% system where lab designers are the owners. The problem that a lab is trying to solve is to separate the false from
% the true claims as well as to identify the strongest true claim for optimization labs.
%  
% Scholars are a second class of platform users that are invited to labs and participate in competitions held in these 
% labs. Binary games are the building block of competitions. A binary game is played by two scholars; one taking the role 
% of proponent and the other taking the role of the opponent. A binary game proceeds as follows: First, the proponent 
% proposes a claim from the family of claims defined in the lab. Then the opponent chooses either to agree with, to
% dispute, or to strengthen the claim proposed by the proponent. In all cases, both the proponent and the opponent 
% participate into at least one refutation game. A refutation game consists of an orderly dialoge between the two 
% players that is used to determine a winner.
% 
% \subsection{SCG Applications}
% 
% \subsection{Contributions}
% 
% \subsection{Paper Organization}
%  
% 
% \section{Paper and Game Mechanics}
% Mastery (When was the last time of contradictions?)
% 
% The analogus situation in chess is to propose a board configuration and make claims that the configuration
% leads to a win in n steps.
%  
% Extract the clever constructions. Scholar evaluation is very useful.
% 
% Working with unreliable scholars
% How do I go about using this platform to design a lab and then how to go about playing a lab?
% Extract the clever constructions. Scholar evaluation is very useful.
% 
% 
% \section{Assessing Scholar Reliability}
% Utilize past performance to assess skill. 
% Elo ratings and many others.
% Uses only latest n games for player.
% 
% 
% We present an an approach to assessing the reliability of scholars that is independent
% of the order of the games.  
% 
% $Rel^{(-1)}(S_i) = 1$\\
% $Wins^{(k)}(S_i) = \sum Payoff(S_i, S_j) * Rel^{(k-1)}(S_j)$\\
% $Losses^{(k)}(S_i) = \sum Payoff(S_j, S_i) * (1 - Rel^{(k-1)}(S_j))$\\
% $Rel^{(k)}(S_i) = Wins^{(k)}(S_i) /(Wins^{(k)}(S_i) + Losses^{(k)}(S_i)) $\\
% 
% Some attractive properties:
% \begin{itemize}
%   \item A player that never looses will have a reliability of 1.
%   \item A player that looses at least a single game, will have his/her reliability hanging on the reliability of other players.
%   \item Loosing a game agianst a player with low reliability will produce a large -ve impact, while loosing a game against a player with a high reliability will have a small -ve impact.
%   \item (The dual) Winning a game against a player with high reliability will produce a large +ve impact, while winning a game against a player with low reliability will have a small +ve impact.
%   \item Order independence. Show that.
%   \item Others?
% \end{itemize}
% 
% \section{The Scientific Community Platform}
% We model scientific knowledge as a set of associations between claims and logical properties. 
% We organize scientific knowledge in labs. 
% A lab defines a family of \emph{refutable} claims with a similar structure. 
% A lab also fixes a particular set of logical properties that players can associate to claims.
% 
% As we rely on crowds to populate the scientific knolwedge, the integrity of the scientific
% knolwedge is jeopardized. We describe a mechanism, called the refutation game, that we can use
% to resolve any conflicts in the scientific knowledge as well as to evaluate players. The refutation
% game mechanism is based on a particular refutation protocol that is part of each claim.
% 
% Finally, we propose a number of potential game mechanims that can be used to stimulate activity on
% our platform.
% 
% \section{Organizing Scientific Knowledge}
% \label{sec:OSK}
% 
% \subsection{Claim}
%  \begin{figure}[htp]
%  \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
% interface Instance {}
% interface Solution {}
% interface QualityFunction 
% 	{ double quality(Instance instance, Solution solution); }
% interface ValidPredicate
% 	{ boolean isValid(Instance instance, Solution solution); }
% \end{lstlisting}
% \caption{Domain Structure}
% \label{code:domainStructure}
% \end{figure}
% 
%  \begin{figure}[htp]
%  \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
% interface Lab 
% 	{ ValidPredicate getValidPredicate();
% 	  QualityFunction getQualityFunction();
% 	  Protocol getProtocol();
% 	  Collection<LogicalProperty> getLogicalProperties();
% 	  Collection<RefutationGameSpecification>
% 	  getRefutationGames(Collection<Assertion> Scholar1assertions, Collection<Assertion> Scholar2assertions);
% 	  Collection<Scholar> getScholars();
% 	  void labMain(); }
% interface LogicalProperty {}
% class Assertion
% 	{ Scholar scholar;
% 	 LogicalProperty property;
% 	 Claim claim; }
% class RefutationGameSpecification
% 	{ Scholar proponent;
% 	  Scholar opponent;
% 	  Claim claim;
% 	  double proponentWinPayoff, 
% 		proponentLossPayoff, 
% 		opponentWinPayoff, 
% 		opponentLossPayoff;}
% \end{lstlisting}
% \caption{Lab and Supporting Structures}
% \label{code:LabStructure}
% \end{figure}
% 
%  \begin{figure}[htp]
%  \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
% interface Claim
% 	{ Lab getEnclosingLab();
% 	  boolean instanceSetPredicate(Instance instance);
% 	  boolean predicate(List<Instance> instances, List<Solution> solutions); }
% \end{lstlisting}
% \caption{Claim Structures}
% \label{code:ClaimStructure}
% \end{figure}
% 
%  \begin{figure}[htp]
%  \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
% interface Scholar
% 	{ /** Propose a claim with a particular logical property
% 	   *  When property is null, any claim can be proposed
% 	   *  The proposed claim must be different from the list of excluded claims*/
% 	  Claim propose(Lab lab, LogicalProperty property, List<Claim> excludedClaims);
% 	  /** Decide which of the lab's logical properties hold for the given claim */
% 	  List<LogicalProperty> decide(Lab lab, Claim claim);
% 	  /** Provide an instance that satisfy the instance set predicate of the claim*/
% 	  Instance provide(Lab lab, Claim claim);
% 	  /** Provide a solution to the instance*/
% 	  Solution solve(Lab lab, Claim claim, Instance instance);
% }
% \end{lstlisting}
% \caption{Scholar Structures}
% \label{code:ScholarStructure}
% \end{figure}
%  
% \section{Game mechanism}
% Players enter into refutation games 
% Desirable properties: Soundness, Liveness (there is some progress finishing lab claims), Fairness.
% 
% Mechanism 1, we get two players, we throw a claim at them. Have them decide on it. Have them play two refutation games.
%   ++ the mechanism and lab owners controls the proposition.
% 
% Mechanism 2, we choose the players, they choose the claims.
% 
% Mechanism 3, the players choose themselves as well as the claims.
% 
% Claims and their relationships:
%   Negation
%   Implication / Generalization / Specialization / Equivalence (binary-relationships)
%   Strength
% 
% We can use claim relationships to expose contradictions in the overall state of knowledge. And to foster interactions.
% We can use claim relationships and players relative positions to expose controversy.
% 
% The point of the mechanism is to match players with claims.
%   
% \section{Applications}
% \subsection{CrowdSourcing Scenarios}  
% Match players with other players and claims (Important to be done right to maintain engagement)
% Evaluate claims and players.
% Related claims

\section{The FSCP Platform}
\label{sec:platform}
A lab in FSCP consists of a claim family and a number of scholars. 
We begin by describing how claim families are specified in FSCP. 
Then we describe how refutation games and substantiation games are derived from claim families. 
Then we describe how scholars interact with the FSCP. 
Finally, we describe few approaches to derive scholar interactions in a lab.

\subsection{Claim Families}
A claim family consists of a logical formula and a model that provides an interpretation of all predicates mentioned in the formula.
A claim consists of an assignment of values from the model to all free variables in the formula. 
Figure~\ref{code:claimFamily:structure} shows the \code{ClaimFamily} and \code{Claim} structures.
 \begin{figure}[htp]
 \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
final class ClaimFamily{
	final Formula f;
	final Model m;
	
	final class Claim{
		final Assignment g;
		...
	}	
}
 \end{lstlisting}
\caption{ClaimFamily Structure}
\label{code:claimFamily:structure}
\end{figure}

\subsubsection{Formulas}
A \code{Formula} is either a simple \code{Predicate}, a \code{Compound} formula, 
a \code{Negated} formula, or a \code{Quantified} formula. A \code{Compound} formula
consists of two subformulas, \code{left} and \code{right} and a \code{Connective} which 
is either an \code{And} or an \code{Or} connective. A \code{Quantified} formula consists
of a \code{Quantification} and a subformula. A \code{Quantification} consists of a \code{Quantifier}, 
two \code{ident}ifiers representing the quantified variable name and type, 
and an optional \code{Predicate} further restricting the values the quantified variable can take. 
A \code{Quantifier} can be either a \code{ForAll}, an \code{Exists}, or \code{Free} which we use to 
declare free variables in a formula. Figure~\ref{code:formula:Language} shows the grammar for a formula
expressed using the class dictionary notation~\cite{DemeterFClassDictionary}.


 \begin{figure}[htp]
 \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
Formula = Predicate | Compound | Negated | Quantified.
Predicate = <name> ident "(" <args> CommaList(ident) ")".
Compound = "(" <left> Formula <connective> Connective <right> Formula ")".
Connective = And | Or.
And = "and".
Or = "or".
Negated = "(" "not" <formula> Formula ")".

Quantified = <quantification> Quantification <formula> Formula.
Quantification = "(" <quantifier> Quantifier <var> ident "in" <type> ident <optionalQuantificationPredicate> Option(QuantificationPredicate) ")".
QuantificationPredicate = "where" <pred> Predicate.
Quantifier = ForAll | Exists | Free.
ForAll = "forall".
Exists = "exists".
Free = "free".
 \end{lstlisting}
\caption{Formula Language}
\label{code:formula:Language}
\end{figure}

\subsubsection{Models}
\label{sec:model}
 \code{Model}s are used to interpret the types and predicates in a given formula.
 Figure~\ref{code:model:structure} shows the \code{Model} interface. It has three
 methods. \code{wellFormedTypeName} checks whether a given type name is supported by
 the model. \code{wellFormed} checks whether a given value is a well formed value of
 a given type in the model. \code{executePredicate} executes a predicate provided by 
 the model.
 
 \begin{figure}[htp]
 \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
interface Model {
	boolean executePredicate(Assignment g, Predicate pred);
	boolean wellFormed(String value, String type); 
	boolean wellFormedTypeName(String type); 
}
 \end{lstlisting}
\caption{Model Structure}
\label{code:model:structure}
\end{figure}

An example of a model is the \code{SaddlePointModel} shown in Figure~\ref{code:model:sample}.
\code{SaddlePointModel} provides one type \code{z1} which is a floating point number between \code{0} and \code{1} 
inclusive. \code{wellFormedTypeName} returns \code{true} only for \code{``z1''}. \code{wellFormed} returns \code{true}
for well formed values of type \code{z1}. The code for \code{executePrediate} supports a single predicate \code{p(z1 x,z1 y,z1 q)}.
This model can be used to interpret for the formula \code{(free q in z1) (forall x in z1)  (exists y in z1) p(x,y,q)}.

 \begin{figure}[htp]
 \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
class SaddlePointModel implements Model{
	public boolean wellFormedTypeName(String type) {
		return type.equals("z1");
	}
	public boolean wellFormed(String value, String type) {
		try{
			float v = Float.parseFloat(value);
			return v>=0 && v<=1;
		}catch(Exception e){
			return false;
		}
	}
	boolean executePredicate(Assignment g, Predicate pred) {
		if(pred.getName().getName().equals("p")){
				
			float x = ...
			float y = ...
			float q = ...
			
			return (x*y + (1-x)*(1-y*y)) >= q; 
			
		}else{
			throw new RuntimeException("Unknown predicate "+ pred.toString());
		}
	}
}
 \end{lstlisting}
\caption{Sample Model}
\label{code:model:sample}
\end{figure}

% \subsection{Claims}
% 
% 
%  \begin{figure}[htp]
%  \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
% final class Claim{
% 	private final Assignment g;
% 	Claim(Assignment g){
% 		this.g = g;
% 	}
% 	RGHistory RG(Scholar verifier, Scholar falsifier){
% 		return RG(f, m, g, verifier, falsifier);
% 	}
% 	RGHistory RG(Formula f, Model m, Assignment g, Scholar verifier, Scholar falsifier ){ ... }
% 	List<SGHistory> substantiationGame(Scholar s1, Scholar.Role s1r, 
% 			Scholar s2, Scholar.Role s2r) { ... }
% }
%  \end{lstlisting}
% \caption{Claim Structure}
% \label{code:claim:structure}
% \end{figure}
% 

\subsection{Scholars}
\label{sec:platform:scholars}
The \code{Scholar} interface describes the inputs that FSCP collects from the crowd. The method \code{decide} is used to collect a decision from
a scholar regarding whether (s)he wants to verify or falsify the given formula under the given model and assignment. Typically, a scholar would want
to be the verifier of claims (s)he believes are true and be the falsifier of claims (s)he believes false. The method \code{choose} is used 
to collect an object from the given model for the quantification variable. Finally, the method \code{propose} is used to collect an assignment for free
variables in the given formula other than the excluded assignments. It is possible to implement the \code{Scholar} interface such that it forwards requests
to human scholars via email or a web interface for example. It is also possible to provide a self sufficient implementation that does not rely on human scholars.
We call such \code{Scholar} implementations, avatars.

 \begin{figure}[htp]
 \begin{lstlisting}[language=java,tabsize=2,breaklines=true,breakautoindent=true]
public interface Scholar {
	public enum Role {
		VERIFIER,
		FALSIFIER
	}
	String getName();
	Role decide(Formula f, Model m, Assignment g);
	String choose(Quantified f, Model m, Assignment g);
	Assignment propose(Formula f, Model m, Collection<Assignment> excluded);
}
 \end{lstlisting}
\caption{Scholar Interface}
\label{code:scholar:interface}
\end{figure}

\subsection{Scholar Interaction}
\label{sec:platform:scholarInteractions}
In FSCP, the interaction between scholars is centered around claims. 
Two scholars can interact by participating in a substantiation game.
Substantiation games build on refutation games which we start explaining 
before we move to substantiation 
a refutation game or a substantiation game.
 
\subsubsection{Refutation Games}
% Adapted from SEP
% 
% 
% In addition to two players P1 and P2, there are two roles:
% verifier and falsifier.
% Initially, P1 is falsifier and P2 is verifier.
% For every predicate logic formula $\phi$, model $M$,
% and variable assignment $g$,
% a two-player zero-sum game $G(\phi,M,g)$ between player P1 and P2
% is defined.
% 
Two scholars taking opposite positions on a specific claim \code{c} can participate in a
refutation game denoted as \code{c.RG(verifier, falsifier)} where \code{verifier} is the scholar
trying to support \code{c} and \code{falsifier} is the scholar disputing \code{c}.

Given a claim \code{c} and two scholars, a verifier $ver$ and a falsifier $fal$. Let $\phi$ be the formula 
and $M$ be the model of \code{c}'s enclosing \code{ClaimFamily}. Let $g$ be \code{c}'s assignment to the free variables in $\phi$.
We define the refutation game of $ver$ and $fal$ centered around \code{c} \code{c.RG(}$ver$\code{, }$fal$\code{)} to be
$G(\phi ,M, g, ver, fal)$ which is a two-player, zero-sum game defined as follows: 

\begin{enumerate}
\item
If $\phi=R( t_1 , ... , t_n)$ and $M,g \models R(t_1 , ... , t_n )$,
$ver$ wins; otherwise $fal$ wins.
\item
If $\phi=!\psi$, the rest of the game is as in $G(\psi, M, g, fal, ver)$. 
\item
If $\phi = (\psi \wedge \chi)$,
$fal$ chooses $\theta \in \{\psi, \chi\}$ and the rest
of the game is as in $G(\theta, M, g, ver, fal)$.
\item
If $\phi = (\psi \vee \chi)$,
$ver$ chooses  $\theta \in \{\psi, \chi\}$ and the rest
of the game is as in $G(\theta, M, g, ver, fal)$.
\item
If $\phi=(\forall x:p(x))\psi$, $fal$ chooses an element 
$a$ from $M$ such that $p(a)$ holds, and the rest of the game is as in \\
$G(\psi, M, g[x/a], ver, fal)$. If $fal$ fails to do so, it loses.
% or a relation a from M (depending on the type of x)
\item
If $\phi=(\exists x:p(x)) \psi$, $ver$ chooses an element 
$a$ from $M$ such that $p(a)$ holds, and the rest of the game is as in \\
$G(\psi, M, g[x/a], ver, fal)$. If $ver$ fails to do so, it loses.
\end{enumerate}

The definition of $G$ is adopted from the Game Theoretic Semantics (GTS) of Hintikka~\cite{GTS-Hintikka},~\cite{sep-logic-if}. We slightly 
modified Hintikka's original definition to handle the quantification predicate in our language. The result of a refutation game consists
of a record \code{RGHistory} of the two scholars \code{verifier} and \code{falsifier}, the \code{winner}, the assignment \code{g}, 
and a \code{timestamp}.
 
\subsubsection{Substantiation Games}
FSCP further extend the potential for interaction between scholars by allowing scholars to participate
in test games even if they are taking the same positions on a specific claim \code{c}. Two scholars \code{s1} and \code{s2} taking two, 
not necessarily contradictory, positions \code{r1} and \code{r2} on claim \code{c} can participate in a substantiation game 
\code{c.SG(s1, r1, s2, r2)}. If the two scholars hold contradictory positions on \code{c}, the substantiation game reduces to a 
refutation game. Otherwise, the substantiation game reduces to two refutation games \code{c.RG(s1, s2)} and \code{c.RG(s2, s1)} 
in which the two scholars teach each other. Given the two positions and the game, Table~\ref{table:scholarUnderTest} can be used to identify the scholar
being tested. It is important to identify the scholar under test for scholar evaluation purposes. The result of a substantiation game
is a list of either one \code{RGHistory} record or two \code{TestHistory} records. A \code{TestHistory} extends \code{RGHistory} records
with a \code{underTest} field. 

\begin{table}
\centering
\begin{tabular}{|c|c|c|c|}
\hline
s1 & s2 & ref game            & tested \\ \hline
v  & v  & \code{c.RG(s1, s2)} & s1         \\
v  & v  & \code{c.RG(s2, s1)} & s2         \\
f  & f  & \code{c.RG(s1, s2)} & s2         \\
f  & f  & \code{c.RG(s2, s1)} & s1         \\
\hline
\end{tabular}
\caption{Scholar Under Test}
\label{table:scholarUnderTest}
\end{table}

\subsection{Labs}
An FSCP lab is a crowdsourcing system that consists of a \\ \code{ClaimFamily} and a 
number of \code{Scholar}s. Furthermore, based on its goal, a lab also provides:
\begin{enumerate}
\item system wide interaction mechanisms for scholars, 
\item an evaluation mechanism for its scholars,
\item a mechanism for combining scholars' contributions.
\end{enumerate}

We discuss system wide interaction mechanisms below and discuss scholar evaluation and 
combination of scholar contributions in 
Section~\ref{sec:scholar:evaluation}.

It is possible to build several system wide interaction mechanisms on top of 
substantiation games and the \code{Scholar} interface. We give here three examples:

\subsubsection{Battleship}
Scholars independently propose claims to the system. When two scholars propose the same
claim, the system collects their position and then engages them in a substantiation game.

\subsubsection{Guided Search}
The system chooses a claim and two scholars, then it collects their positions on 
that claim and engages them in a substantiation game. The system repeats until it reaches
its goal. For example, suppose that we are building a crowdsourcing system to find the
critical point of some free variable (from an ordered domain) in a formula. This is the value 
such that all claims above it are, for example, false. The system can effectively 
perform a binary search on the domain of that free variable. At each step in the binary 
search, the system creates a claim and chooses two scholars and engage them in a substantiation game.

\subsubsection{Scientific Community Game}
The Scientific Community Game (SCG) is a precursor to FSCP. The focus of SCG was educational.
In SCG, scholars play a soccer-like tournament of binary matches. A match consists of an even number 
of rounds where scholars participate in binary games with alternating roles. SCG binary games are a precursor 
to substantiation games. 
In an SCG binary game, a scholar called the proponent proposes a claim. By doing so, the proponent is implicitly taking
the verifier position on the claim it proposed. Then the other scholar, called the opponent, is asked to 
decide whether it agrees or disputes the claim. In either case, both scholars participated in a refutation game.

Eventually, a scholar ranking is produced as well as a trace of all refutation games. The intent was that scholars learn 
from the traces and the ranking is used to motivate them.
   
%Given a \code{ClaimFamily} and a number of \code{Scholar}s

\section{Scholar Evaluation}
\label{sec:scholar:evaluation}
In a platform like FSCP, there are many qualities that we can measure and evaluate scholars based on. 
For example, we can measure the scholar's activity by counting the number of games it had played.
We can measure the scholar's originality by counting the number of breakthroughs such as being the first 
to propose and verify a particular claim or being the first to falsify a claim.
We can measure the scholar's learning during a particular period of time by comparing its rank at the 
beginning and at the end of that period.

Since the purpose of FSCP labs is to accurately classify claims. We are interested in measuring scholar's 
\emph{reliability} which we define as scholar's likelihood of deciding to be the verifier of true claims and 
the falsifier of false claims. One approach to measure reliability is through testing the scholar's performance 
against a gold standard.

Instead, we measure scholar's \emph{strength} which we define as the scholar's ability to push its opponent
into self-contradiction. In Table~\ref{table:scholarPayOff}, column ``cont." provides an extensive list of 
the situations in which a scholar becomes self-contradictory. These situations can be summarized as losing 
a refutation game that is not played for testing as well as losing a refutation game while being the scholar 
under test. In both situations, the scholar contradicts its original position on the claim.

We prefer to measure \emph{strength} instead of \emph{reliability} because:
\begin{itemize}
  \item strength is highly correlated to reliability. In order to increase their strength, scholars need to push
		their opponents into self-contradiction. To do so under the zero-sum nature of the game, scholars need to 
		avoid falling intro self-contradiction themselves. To do so, scholars need to be reliable because unreliable
		scholars risk falling into self-contradictions. Especially, in the presence of other strong scholars. 
		This can be seen from Table~\ref{table:scholarPayOff}.
		
 \item It is free to accurately measure strength while it can be expensive to measure reliability. To directly 
 		measure reliability, we need to either higher experts to provide a gold standard or have some claims redundantly
 		examined by several scholars.   
\end{itemize}  
% 
% 
% For that purpose, \emph{strength} is the most important quality. We define scholar \emph{strength} to be its 
% ability to push their opponents into self-contradictiction, rather than taking the correct position on claims.
% We prefer scholar strength to scholar reliability
% 
%  
% Because, if FSCP is used in a research setting, then this implies that there is no
% known decision procedure for the given \code{ClaimFamily}. If FSCP is used in an
% educational setting, then it is important not only that scholars know which claims are
% true or false but also know how to support it too.
% 
% %\subsection{Self-contradictory Scholars}
% A scholar that loses a refutation game that is not played for testing contradicts
% its original position and therefore is self-contradictory. Likewise, a scholar that loses
% a refutation game while being the scholar under test contradicts its original position
% and therfore is self-contradictory. A scholar that never falls into self-contradiction is 
% called a perfect scholar.
% 
% %\subsection{Reliable Scholars}
% A scholar that always chooses to verify true claims and chooses to falsify false claims is
% called a reliable scholar. A reliable scholar can still fall into self-contradictions and 
% a perfect scholar is not necessarily reliable. However, by taking an incorrect position on 
% claims, scholars risk being contradictory especially 1) on the long run. 2) in the presence 
% of other strong scholars. Therefore, scholar reliability is highly correlated to the scholar's 
% likelihood of being non self-contradictory.

We designed the payoff matrix so that it only rewards a scholar with a point when the scholar
successfully pushes its opponent into self-contradiction. This can be seen from Table~\ref{table:scholarPayOff}.

\begin{table}
\centering
\begin{tabular}{|c|c|c|c|c|c|c|c|}
\hline
s1 & s2 & ref game            & tested & winner & cont. & s1 & s2 \\ \hline
v  & v  & \code{c.RG(s1, s2)} & s1         & s1     &       -       &    0      &      0    \\
v  & v  & \code{c.RG(s1, s2)} & s1         & s2     &       s1      &    0      &      1    \\
v  & v  & \code{c.RG(s2, s1)} & s2         & s1     &       s2      &    1      &      0    \\
v  & v  & \code{c.RG(s2, s1)} & s2         & s2     &       -       &    0      &      0    \\ 
\hline
f  & f  & \code{c.RG(s1, s2)} & s2         & s1     &       s2      &    1      &      0    \\
f  & f  & \code{c.RG(s1, s2)} & s2         & s2     &       -       &    0      &      0    \\
f  & f  & \code{c.RG(s2, s1)} & s1         & s1     &       -       &    0      &      0    \\
f  & f  & \code{c.RG(s2, s1)} & s1         & s2     &       s1      &    0      &      1    \\ 
\hline
v  & f  & \code{c.RG(s1, s2)} & -          & s1     &       s2      &    1      &      0    \\
v  & f  & \code{c.RG(s1, s2)} & -          & s2     &       s1      &    0      &      1    \\
f  & v  & \code{c.RG(s2, s1)} & -          & s1     &       s2      &    1      &      0    \\
f  & v  & \code{c.RG(s2, s1)} & -          & s2     &       s1      &    0      &      1    \\ 
\hline
\end{tabular}
\caption{Payoff Matrix}
\label{table:scholarPayOff}
\end{table}

\section{Measuring Scholar Strength}
We present an algorithm to measure the strength of scholars that is independent
of the order of the games based on the payoffs that scholars received. 
The function $Payoff(S_i, S_j)$ returns the number of times scholar $S_i$ has pushed scholar $S_j$ into self-contradiction.
  
$Str^{(-1)}(S_i) = 1$\\
$Wins^{(k)}(S_i) = \sum Payoff(S_i, S_j) * Str^{(k-1)}(S_j)$\\
$Losses^{(k)}(S_i) = \sum Payoff(S_j, S_i) * (1 - Str^{(k-1)}(S_j))$\\
$Str^{(k)}(S_i) = Wins^{(k)}(S_i) /(Wins^{(k)}(S_i) + Losses^{(k)}(S_i)) $\\

The algorithm starts with an estimate of $1$ for the strength of all scholars. 
Then it computes the weighted wins and losses for each player based on the payoffs and the strength of their opponents.
Then it computes strength as the fraction of weighted wins divided by the sum of weighted wins and losses.
The last two steps are iterated to a fixpoint.

The proposed algorithm has the following attractive properties:
\begin{itemize}
  \item A scholar that never looses will have a strength of $1$.
  \item A scholar that looses at least a single game, will have his/her strength hanging on the strength of other scholars.
  \item Loosing a game against a scholar with low strength will produce a large -ve impact, while loosing a game against a scholar with a high strength will have a small -ve impact.
  \item (The dual) Winning a game against a scholar with high strength will produce a large +ve impact, while winning a game against a scholar with low strength will have a small +ve impact.
  \item Order independence.
%  \item Others?
\end{itemize}


\subsection{Truth Likelihood of Claims}
 The basic idea is to accumulate evidence about the truth and falseness of claims. 
 Scholars provide evidence through picking positions on claims as well as through winning refutation games.
 Scholar strength is used to weigh their evidences.
 
For each claim $c$ we associate two positive real numbers $c_T$ and $c_F$ with it. The higher $c_T$ the more likely
$c$ is true. The higher $c_F$ the more likely $c$ is false.
If $c_T > c_F$ then 
\[ L(c) = (c_T-c_F)/c_T \] is the likelihood that $c$ is true.
And $1-L(c)$ the likelihood that $c$ is false.
If \( c_F \geq c_T  \) then 
\[ L(c) = (c_F-c_T)/c_F \] is the likelihood that $c$ is false.
and $1-L(c)$ the likelihood that $c$ is true.
 
At the beginning of a substantiation game for claim $c$, we adjust $c_T$ and $c_F$ as follows:
For each scholar $s$ taking the position of a verifier of $c$ we add $str(s)$ to $c_T$.
Similarly, for each scholar $s$ taking the position of a falsifier of $c$ we add $str(s)$ to $c_F$.

After a refutation game in which the verifier scholar $ver$ loses, we add $str(ver)$ to $c_F$.
Similarly, after a refutation game in which the falsifier scholar $fal$ loses, we add $str(fal)$ to $c_T$.
The intuition is that the losing player must have done its best to avoid the loss while the winning scholar
might not have done its best to win.

% \subsubsection{Simple Voting for Claims}
% 
% 
% \begin{itemize}
% \item
% The claim is supported.
% Scholar $s$ votes claim $c$ to be true because $s$ defended it against $!s$. 
% % s!ST (the stronger !S the more likely c is true).
% % sST (the stronger S the more likely c is true).
% Support happens for {\bf As} and {\bf DPs} and we update $c_T$ as follows:
% %\[ c_T = c_T + max(rel(O),rel(P)).\]
% \[ c_T = c_T + rel(O)+rel(P).\]
% The stronger $P$ or $O$ the more likely $c$ is true.
% \item
% The claim is refuted.
% Scholar $s$ votes claim $c$ to be false because $s$ refuted it.
% Refutation happens for {\bf ARPA} and {\bf Doro} and we update $c_F$ as follows:
% %\[ c_F = c_F + max(rel(O),rel(P)).\]
% \[ c_F = c_F + rel(O)+rel(P).\]
% The stronger $P$ or $O$ the more likely $c$ is false.
% \end{itemize}
% 
% \subsubsection{Better 3-Component Voting for Claims}
% There is a better way of voting for the truth of claims which takes
% more context into account than just the fact whether a claim
% was refuted or defended.
% 
% %Reputation computation:
% %Initially all have rep(S) = 1.
% %We assume the payoff function payoff(S) to be non-negative.
% %update of reputation after a binary game:
% %rep(O) = rep(O) + payoff(O)*rep(P)
% %rep(P) = rep(P) + payoff(P)*rep(O)
% %
% %For special case 
% %when S not blamed, the payoff is 1
% %when S is blamed, the payoff is 0
% %we get:
% %rep(S) = rep(S) + rep(!S) when S not blamed
% %rep(S) stays the same when S blamed.
% 
% The 3-Component voting is based on the 3 levels of  the binary game:
% 
% \begin{enumerate}
% \item
% The proponent $P$ votes the claim to be true. Weight of vote: $rel(P).$
% \item
% If $O$ decides {\bf a} (agree), it votes for the claim to be true.
%    If $O$ decides {\bf d} (dispute), it votes for the claim to be false.
%    Weight of vote: $rel(O).$
% \item
% The game makes a vote based on the outcome as follows (we used only this above):
%    If {\bf *s{\it s}} (support by $s$), the game votes the claim to be true. 
%    if {\bf *r{\it s}} (refute by $s$), the game votes claim to be false.
%    Weight of vote: $rep(!s).$
% \end{enumerate}
% For the four cases we get:
% \begin{itemize}
% \item {\bf As:}
% $c_T = c_T + rel(P) + rel(O) + rel(P)$,
% $c_F $ unchanged
% %true wins.
% 
% \item{\bf ARPA:}
% $c_T = c_T + rel(P) + rel(O),
% c_F = c_F + rel(O)$
% %true wins
% 
% \item{\bf Doro:}
% $c_T = c_T + rel(P),
% c_F = c_F + rel(O) + rel(P)$
% % false wins
% 
% \item{\bf DPs:}
% $c_T = c_T + rel(P) + rel(O), 
% c_F = c_F + rel(O)$ 
% %true wins
% \end{itemize}
% 

\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 reformatory
actions on piazza.com.
We used a multi player 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 JASON
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-Shapely 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}
\subsection{Crowd Sourcing and Human Computation}
\subsubsection{Dealing with Unreliable Workers}
Most crowdsourcing systems must devise schemes to increase
confidence in the worker's solutions to tasks, typically by 
assigning each task multiple times \cite{DBLP:conf/nips/KargerOS11}. Larger et AL. present a general model for crowdsourcing
tasks.
In FSCP, because workers need to justify their answers in a game
against another worker, unreliable workers will run
into many contradictions and get a low rating. This means
that their votes will minimally affect the final result,
the knowledge base of true claims.

\cite{RankingAggregation2013} is related to
FSCP scholar ranking.
The algorithm is an extended Bradley-Terry model called Crowd-BTU. 
The paper focuses on finding the quality of annotators in a crowdsourced setting.
They study the exploration-exploitation tradeoff
which is also relevant to FSCP for labeling claims
as true or false.

The "Evaluating the Crowd with Confidence" paper
\cite{ilprints1051} has a title that seems very
applicable to FSCP. However, they use a model which
is too simple for FSCP.
In particular, in FSCP the errors depend on task 
difficulty, and worker errors are not independent
of each other because they play a game.

\subsubsection{Rating Systems}
We use a rating system
for games with wins, losses and draws.
This subject has been studied for a long time
and there are many applications of rating systems.
For example, in chess and other sports,
the Elo rating system is used.
A good survey and critique of rating systems is given in
\cite{Beasley-Mathematics-Games}.
%rating
%measure actual skill of scholars
%grade of scholar
Rating systems are a controversial subject and there are many
algorithms that can be used.
TopCoder \cite{TopCoder}
uses an Algorithm Competition Rating System to rank the coders.

%unweighted
%weighted means
%using the last n results
%
%measure of performance
%measure of ability


\subsubsection{Combining Worker's Contributions}

In FSCP, we use two approaches to combine scholar
contributions: (1) 
During the refutation games, the scholars
give each other feedback by trying to drive
each other into a contradiction. This is a collaboration
which leads
potentially to new ideas and knowledge fusion.
(2)
In FSCP, scholars vote on the truth or falseness of claims when deciding to verify or falsify claims.
Furthermore, it is not enough for scholar to just vote but also it is important that they justify their votes through their actions in refutation games. 
We combine the votes with justifications into
an overall vote for whether a claim is true.
Related work is
\cite{RankingAggregation2013} and
\cite{DBLP:conf/nips/KargerOS11} which was 
already discussed above.

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

The FSCP 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 FSCP 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 FSCP.
\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 FSCP,
but a big part of the tutorial is reusable
across scientific disciplines.

\subsubsection{Crowdsourcing complex tasks}

\cite{Kittur:2011:CCC:2047196.2047202} describes a general-purpose framework
for solving complex problems through micro-task markets.
Engaging in the scientific dialogs of FSCP could be done through
a micro-task market.
\cite{minder2011crowdlang} proposes a language to
define crowdsourcing systems. Our lab definition approach 
provides a declarative description of what needs to be
crowdsourced.

\cite{kosinski:crowd} provides an interesting analysis of
several issues relevant to FSCP: how incorrect responses should affect worker 
reputations and how higher reputation leads to better results.

\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 FSCP 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 FSCP?
%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 FSCP 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 FSCP 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 FSCP 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 FSCP has this property and provides a specific 
architecture for building knowledge bases in
(formal) sciences. 
Collaboration between scholars is achieved through
the scientific discourse implied by the refutation game.
%which exchanges instances
%and solutions. 
The information exchanged
gives hints about how to play the game better next time.
%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 FSCP 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. 
Topcoder.com 
\cite{TopCoder} 
includes an
online  judge capability, but where the inputs are provided by competitors. 
This dynamic benchmark capability is also expressible with the FSCP: 
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 FSCP 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 makes the scientific discourse more challenging.
%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 FSCP experiments are performed when the game
associated with a claim is elaborated.

Karl Popper's work on falsification
\cite{nla.cat-vn1027910}
is the father of non-deductive methods in science.
The FSCP 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 FSCP 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 FSCP, 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 FSCP 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{SCG}
SCG~\cite{scg-bionetics},~\cite{scghome},~\cite{scg-def} is a close predecessor of FSCP.
% 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.

% \cite{scg-def} describes an earlier version
% of SCG. 
The key difference between FSCP and SCG is that SCG was 
targeted at evaluation of the scholars while 
FSCP is targeted at crowdsourcing true claims.
FSCP is cleaner: there is a simple concept of self-contradiction
and there is no longer a need to have the concept of strengthening
a claim explicitly.

%\begin{itemize}
%\item{Claims are more expressive}
%
%In \cite{scg-def}, claims are defined in terms of
%a protocol which can simulate predicate logic
%formulas in prenex normal form.
%In this paper, the use of predicate logic to express
%claims which makes it easy to express properties
%of claims such as: this claim is optimal.
%The use of predicate logic also facilitates
%a future switch to Independence-Friendly Logic
%\cite{sep-if} which provides a general solution
%to deal with incomplete information.
%In \cite{scg-def} there is support for incomplete
%information but it is not general.
%An Independence-Friendly Logic formula is translated into
%a refutation game in a similar way as a predicate
%logic formula.
%\item{Substantiation game is simpler}
%
%In \cite{scg-def}, there were several kinds
%of contradictions while in this paper there are only two:
%VerifierLost and FalsifierLost. 
%The Conflict Resolution Games and the Testing Games
%are now simpler and general.
%For testing, we have now two refutation games while in
%\cite{scg-def} there was only one.
%It is important that both scholars get tested.
%\item{Game properties are easier to prove}
%
%The game properties and associated definitions
%are easier to state. The proofs are simple.
%%
%The key definitions are:
%(1) A contradictory scholar either loses a conflict resolution game or a test game while under test.
%(2) A reliable scholar only chooses to verify true claims and falsify false claims.
%(3) A perfect scholar never shows contradictory behavior.
%The key properties are:
%(1) Unreliable scholars risk to be contradictory.
%(2) Perfect scholars are reliable.
%\end{itemize}

\section{Conclusion and Future Work}
\label{sec:conc:fw}
We presented FSCP, a crowdsourcing platform for formal science.
FSCP provides a simple interface to
a community that uses the (Popperian) Scientific Method.

We want to extend our model so that we can make claims about claims.
For example, we want to have a "macro" for a claim to be optimal.
We want to leverage claim relationships across labs
and work with lab reductions as a useful problem
solving tool.

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, FSCP will make contributions to computer-assisted 
problem solving.

% \section{Conclusions}
% \label{ConclusionSection}
% We presented FSCP, a crowdsourcing platform for formal science.
% FSCP provides a simple interface to
% a community that uses the (Popperian) Scientific Method.
% The FSCP 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.
% 
\section{Acknowledgments}
We would like to thank Magy Seif El-Nasr, Casper Harteveld, Thomas Wahl and Tugba Koc for their input to the paper. % \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
% 


% \input{crowd-sourcing}
% \input{pattern-applications}
% %\input{definitions2}
% \input{learning}
% \input{problem-solving}
% \input{convergence}
% \input{accidental-refutation}
% \input{rules}
% \input{example}
% \input{related}

%\cite{StanfordEncyclopedia}

%\bibliographystyle{abbrv}
%\bibliography{sample}

\bibliographystyle{abbrv}
\bibliography{references}

% \input{executive-summary-nsf}
\end{document}
