%%This is a very basic article template.
%%There is just one section and two subsections.
%\documentclass[9pt]{article}
%\documentclass[preprint,12points]{sigplanconf}
%\documentclass[preprint]{sigplanconf}
%\documentclass[letterpaper]{article}
\documentclass[twoside,11pt]{article}
%\documentclass[12pt]{sigplanconf}

\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\concern}[1]{\textbf{(CONCERN #1)}}
\usepackage[titletoc,toc,title]{appendix}
\usepackage{comment}
\usepackage{listings}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm} %Theorems and definitions
\usepackage{multirow}
%\usepackage{hyperref}
\usepackage{float}
\usepackage{graphicx}
\usepackage{comment}

% Required Packages 
%\usepackage{aaai}% 
\usepackage{jair, theapa, rawfonts}
\usepackage{times} 
\usepackage{helvet} 
\usepackage{courier} 
\setlength{\pdfpagewidth}{8.5in} \setlength{\pdfpageheight}{11in}

%\lstset{basicstyle=\small}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}

\title{Collusion-Resistant Evaluation
of Side-Choosing Games 
%with Applications to Competition Organization and Teaching
}
\begin{comment}
\author{Ahmed Abdelmeged \and Karl Lieberherr \and Ruiyang Xu\\ Northeastern University, CCIS, Boston \\ 
mohsen@ccs.neu.edu, lieber@ccs.neu.edu,
ruiyang@ccs.neu.edu}
\end{comment}
\author{\name Ahmed Abdelmeged \email mohsen@ccs.neu.edu \\
\name Karl Lieberherr \email lieber@ccs.neu.edu\\
\name Ruiyang Xu \email ruiyang@ccs.neu.edu \\
	   \addr College of Computer and Information Science,\\
Northeastern University,\\
440 Huntington Avenue,\\
202 West Village H,\\
Boston, MA 02115, USA}

\begin{document}
\maketitle

9-22-2014

\begin{abstract}

Very OLD.

We describe a proof of concept implementation of a CAG-based crowdsourcing platform for formally-specified computational problems, called the Scientific Community Game (SCG).
SCG uses a modular construct, called a lab, to group related claims and to solve labs incrementally through lab relations, 
which are themselves captured as labs.
SCG has the flavor of a "Wikipedia for Computations" 
where inventions are explicit and composable;

Our proposed system has significant applications, in addition to
crowdsourcing formally-specified computations.
(1) The collaborative and self-evaluating nature
of SGs provides a peer-based evaluation system
for MOOCs on formal science topics. The peer-based evaluation
is guaranteed to be fair, and it saves significant time for the teaching staff.
(2) SGs provide a lower barrier of entry to making contributions 
to formal sciences
through game play. It is a significant help to scientists
to test claims using the crowd.

\end{abstract}


\section{Introduction to Side-Choosing Games}
% game and debate are synonyms
\cite{AhmedThesis} Side-choosing games are a new kind of game where the first move
is simultaneous and involves
choosing a side on a position $p$ that comes from another two-person game 
without draws, called a reference game.
The choice is about two possibilities:
\begin{itemize}
\item
$p$ is a winning position, i.e., there is a winning strategy, and, 
\item
$p$ is a losing position, i.e., there is no winning strategy.
\end{itemize}
We call the first decision to take the {\em proponent} role 
and the second decision to take the {\em opponent} role on $p$.

% debates
Side-choosing games model debates on a topic $p$.
Either you are for $p$ (proponent) or you are against $p$ (opponent).
Your choice must be an informed choice: you must be ready to
play an actual game from position $p$ and perform according to your side choice.
When the reference
game $p$ is played between two participants, one participant
is in proponent role and the other in opponent role.
If you are proponent you must win in the proponent role and if
you are opponent you must win in the opponent role.
If participant $x$ does not perform according to its choice,
we say that the participant was brought into a contradiction.
We use the impersonal reference ``it'' because participant may just be software.

% devil's advocate
We explicitly model the situation where both participants want to
be proponent or  both want to be opponent on position $p$. Because the game 
requires one participant in proponent role and the other in opponent role,
we put one participant in devil's advocate role by forcing him or her
to take the opposite side that was chosen.
Therefore, we record game results using the following kind of table:
\begin{verbatim}
Make a Latex table

  W  L  Forced
1 x  y  x
2 x  y  y
3 x  y  none
4 y  x  x
5 y  x  y
6 y  x  none
\end{verbatim}
Column $W$ is for winners, column $L$ for losers and column $Forced$
indicates who was forced (played in devil's advocate role).
The winner or loser may be forced or {\em none}.
In debate 1, $x$ won in forced side while $y$ lost in non-forced side.
This is not a good outcome for $y$ and we say $y$ had a fault because it
lost in non-forced side. Also in debate 3, participant $y$ had a fault.

% relevance
Why are side-choosing games interesting? They model many interesting 
practical debate situations. For example, the position $p$ could be
a claim formulated in a specific structure using a logical sentence.
Side-choosing games are very simple: they are based on the concepts
of winning, losing and forced, yet
we can prove useful
theorems about them. Those theorems allow us to make informed
choices in many different application domains.

% nature of claims
What is the nature of the theorems that we prove. They are
theorems about tables (like the table above) and their mappings to 
rankings. A ranking is a total relation between the participants.
The theorems make predictions about adding rows
with specific properties to the tables
and how they affect the rankings.
These predictions are useful because they allow us to predict that certain
rating changes are impossible.

\subsection{Participant Evaluation}
Our objective is to find the most meritorious
participants given a table of debate results. 
An alternative would be to go for the positions that 
are predominantly successfully defended or opposed.
But we prefer the meritocratic approach which is more robust
for reasons that we don't discuss in this paper.
Once we have the most meritorious participant we can use it
to decide and defend/refute the claims.

The first approach is a centralized approach where there is 
a centralized participant that "knows the truth" and 
that will evaluate the regular participants. The centralized
approach has the problem that it is costly to develop the centralized
participant.

We prefer a distributed approach which uses games between the
participants. However there a few obstacles to overcome.
When the participants evaluate each other there are a few dangers:
(1) the evaluation may not be objective. The participants might have 
favorites.
(2) multiple participants might collude to damage another participant.
For (2) we have collusion-resistant ranking functions and for (1)
we use
contradiction-agreement games.
But our collusion-resistant ranking functions create their own
problem for which we have a solution too: 
The collusion-resistant ranking functions make the players hide in a corner
avoiding to play debates.
The collusion-resistant ranking functions don't incentivize 
the participants to play.
We use a scheduler to force the debates that are needed 
for a fair evaluation.


\subsection{Prominent Application}

Semantic games

\section{Related Work}
\subsection{Side-Choosing Games}
Many different game forms have been studied
but the general concept of a side-choosing game seems to be new.

\begin{verbatim}
http://www.phil.uni-mannheim.de/fakul/phil2/rueckert/pdf/WDL_Rohfassung.pdf
\end{verbatim}

In semantic games, the notion of choice and supporting
the choice one has made is an important theme.

Dialogical Logic.
Erlangen School founded by Paul Lorenzen. Methodical Constructivism.

But the abstraction of a side-choosing game was not needed
back then because there was no web that makes it 
easy to execute, record and check such games.
Back then there was no need for tournaments of such games
and there was no danger of collusion.

Our concepts of forcing, control and collusion-resistance
are new and so is our axiomatic theory involving those concepts.


\subsection{Axiomatic Treatment of Ranking Functions}

In ~\cite{Rubinstein1980}, Rubinstein provides an axiomatic treatment of tournament ranking functions that bears some resemblance to ours. 
Rubinstein's treatment was developed in a primitive framework where ``beating functions'' are restricted to complete, asymmetric relations. 
Rubinstein showed that the points system, in which only the winner is rewarded with a single point is \emph{completely} characterized by 
the following three \emph{natural} axioms:
\begin{itemize}
  \item anonymity which means that the ranks are independent of the names of participants, 
  \item positive responsiveness to the winning relation which means that changing the results of a participant $p$ from a loss to a win, guarantees that $p$ 
  		would have a better rank than all other participants that used to have the same rank as $p$, and
  \item Independence of Irrelevant Matches (IIM) which means that the relative ranking of two participants is independent of those matches in which neither is 
  		involved. 
\end{itemize}
Our LCE axioms are, in some sense, at least as strong as Rubinstein's IIM because, according to LCE, the relative rank of some participant $p_x$ w.r.t. 
another participant $p_y$ cannot be worsened by games that $p_x$ does not participate in nor can it be improved by games that $p_y$ does not participate in. 

In~\cite{axiomaticApproachToRanking}, the authors provide an axiomatic study of several ranking functions that are based on rating methods.
Eight ranking methods, including the points system, and fourteen different axioms, including Rubinstein's IIM, are studied in the paper.
Each of the ranking methods is analyzed to determine the axioms it possesses. Only the points system possesses the IIM axiom. 
The IIM axiom is, however, considered to be an undesirable axiom to have because it is thought to prevent the ranking function from making up for any 
advantage given to certain participants by a tournament schedule that contains only a subset of the games that would be played in a round robin tournament.  
Again, none of these ranking functions is specifically developed for SG tournaments. Also, we use a round-robin-like tournament and IIM-like axioms are not 
undesirable to have. 

\subsection{Tournament Ranking Functions}

Rating methods can be used to rank tournament participants.
There is a vast body of literature on the topic of \emph{heuristic}~\cite{MathematicsOfGames} rating methods aiming to estimate the skill level of 
participants such as the Elo~\cite{elo} rating method. ~\cite{whosnumber1} gives a recent comprehensive overview of rating methods used in sports 
tournaments.
Our work differs from this vast body of literature in two important aspects. 
First, our axioms and ranking method are the first to be developed for an extended framework that we developed specifically to 
capture some of the peculiarities of SG tournaments such as side choice and forcing.
Second, our work is the \emph{first} to be concerned with collusion resilience.


\section{Formal Definitions}
{\bf We are defining the terminology for a new field of side-choosing games. 
We better choose the terminology carefully so that it will be adopted by others.}
Proposed renamings from the dissertation:
\begin{verbatim}
OLD			NEW
LCE			CR (collusion-resistant)
beating function SCG-table
NNRW NNEW
NPRL NPEL
Regard Effect
\end{verbatim}

plan for ordering definitions
\begin{verbatim}
SCG and SCG-tables
Total Preorders
Scoring Functions
Rankings
Axioms
  NNEW
  NPEL
  CR
Monotonicity Constraints
  NNEW and NPEL using monotonicity constraints
  Defining CR using monotonicity constraints
  Equivalence to previous CR definition
\end{verbatim}
The paper is organized as follows:
We first describe the challenges behind the problem that we solve
and we give a heuristic argument for the result we prove formally.
In section ?? we give the key definitions from SCG, SCG-tables,
axioms and monotonicity constraints and how we use them 
to express the axioms. Section ?? describes the main result,
a representation theorem for ranking functions satisfying the axioms.
We give two proofs, one based on monotonicity constraints and the other on the analysis of a Venn diagram describing game results.
In section ?? we apply side-choosing games to 
organize competitions using semantic games, a special kind 
side-choosing game. (Let's see whether we have enough room 
to describe this for the AAAI conference)

\subsection{Side-Choosing Games}

\begin{verbatim}

Side-ChoosingGame = Side-Choice x GeneralSemanticGame
• GeneralSemanticGame: details of protocol not important 
	• Game outcome must satisfy certain rules
• Winning strategies

Examples of families of semantic games
• Logics
	• concrete example: Integer inequality.
• Positions in explicit-form games
	• concrete example: Chess: mate in two.

Meritocracy management
• Tables with base and derived fields
• Important table: SCG-Table: (W,L,F)
	• SCG-Rows
• How to get to the SCG-Table?
\end{verbatim}
Side-choosing games come from a generalization of semantic games with side-choice mechanism. Before we give out the definition of side-choosing games, we shall first have a look at a definition of semantic games in Logic and Epistemology (by A-V Pietarinen):
\begin{verbatim}
DO WE STILL NEED THIS DEFINITION?
\end{verbatim}
\begin{itemize}
\item Two players confront one another, facing a claim and observing a set of rules telling them which moves are legal.
\item They both try to win the game by proving any side of claim (i.e. be a proponent or opponent of the claim), and if one of them finds a systematic way of doing so, he or she has a winning strategy.
\item The set of game rules is fixed by the logically active components in language. In the case of first-order languages the logically active components comprise the existential and universal quantifiers.
\end{itemize}

Generally speaking, A game is defined by game states, moves and the rules when the moves are applicable. The definition of side-choosing games is a generic definition built on mapping logical sentences in predicate-logic to games so that a property holds about truth of the sentences and the existence of winning strategies. The outcome of a side-choosing game gives the winner, looser and information about who was forced.

Side-choosing game consists of two parts: 
\begin{itemize}
\item Simultaneous design-time decision, this is the design time for the winning strategy for Proponent/Opponent.
\item Run-time decision (imposed from outside) followed by sequential game defending run-time decision. This is the decision used when the defense game executes and might involve forcing at most one participant. Specifically, once both players take same side, then choose one of the two players randomly. Here we use a state variable: already\_forced. Goal is to force one by one and play two games. So if there are two "not already\_forced", choose one of the two players, and force the player; if one "not already\_forced", force that one.
\end{itemize}

Next, we discuss the side-choice mechanism in detail here: since we don't want both players choosing the same side, that means, given a claim, one of them must be a proponent and the other be a opponent, one of them must be forced to change to the other side while both of them have found the winning strategy for the same side. Briefly speaking, if both the players have chosen the same side, a Run-time decision must be imposed.

Here we introduce the Agreement Map: The agreement function maps two players x,y with their design-time side choices $(d_x,d_y)$ into a set of games between the two players with run-time side choices $(r_x,r_y)$. A specific agreement function is called CAG (Competitive Agreement Game), which is designed for tie-break when both players have chosen the same side ($d_x=d_y$); We choose the forced player randomly to balance the potential disadvantage. Then we play two games to give each player a chance to test the other:
\begin{itemize}
\item Choose a design-time side: P or O: dx, dy for G. P means: The start position of G is a winning position for player in P role. O means: The start position is not a winning position for player in P role.
\item If $dx \neq dy$: play game $SCG(G, x, y, d_x, d_y, d_x, d_y)$
\item Else: Use agreement map AM to determine games to be played. Each game is of the form $SCG(G, x, y, d_x, d_y, r_x, r_y)$ for run-time side-choices $r_x$, $r_y$ determined by the agreement map AM.
\end{itemize}

We record the game results with only the information of who was the proponent and who won the game. There are actually four cases of game result in terms of any specified play x (Figure \ref{fig:semanticCases}):
\begin{figure}[H]
\centering
\includegraphics[width=0.3\textwidth]{SemanticCases.png}
\caption{\label{fig:semanticCases} Semantic game result cases in terms of player x}
\end{figure}

Considering the side-choice mechanism, the original side chose by each player should also be recorded. Then combined with game result information above, one can infer who has been forced. It's easy too see that there are only four cases of side-choice, and if both players chosen the same side, one of them must be forced to change side (Figure \ref{fig:sideChose}):
\begin{figure}[H]
\centering
\includegraphics[width=0.3\textwidth]{SideChose.png}
\caption{\label{fig:sideChose} Side-choice cases in terms of player x and not x}
\end{figure}

Given the game result and side-choice information, one can derive further information about the game such as who is the loser? Is there anyone forced? Who is forced? We call this game result table with derived information as Concrete SCG-Table. And since we only care about the information of winner, loser and forced side-choice, dropping out other information we abstract the Concrete SCG-Table to what we want, and we called the abstracted new table SCG-table (Figure \ref{fig:SCGrelations}):
\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{SCGrelations.png}
\caption{\label{fig:SCGrelations} How SCG-table derived from semantic games and side-choice}
\end{figure}

Now we can give out the definition of side-choosing game:
\begin{itemize}
\item SCG is a tuple: (CG,AM), where CG is a two-person combinatorial game and AM is an Agreement Map.
\item The game is between two players and starts with a position (node) q in CG for which the two players choose a side.
\item Either a single game is played  (different sides) or AM is activated (same sides) and one or more games are played.
\item The results of the games are recorded in the form W,L,F.
\end{itemize}

\begin{comment}
Now we can give out the definition of side-choosing game: The game is about a claim C involving a set of players Players. First move is simultaneous -- choose a side: Proponent (P) or Opponent (O). 
\end{comment}

Each game result then produced as an SCG-row in an SCG-table. It's reasonable to show that the game out comes shall follow certain rules (SCG-Table Rules), if it's a side-choosing game:
\begin{itemize}
\item Columns are: W,L,F (for Winner, Loser, Forced) (SCG-Table Rule 0).
\item W,L contain either one of the player but W≠L. There are no ties (SCG-Table Rule 1).
\item F contains “none” or W or L. A participant is forced if it has to take the opposite side (SCG-Table Rule 2).
\item Multiple rows may involve the same two participants (SCG-Table Rule 3)
\item Each row presents only one game result between two distinct participants in players set (SCG-Table Rule 4).
\end{itemize}

One thing to notice is that the SCG-table definition does not specify any legal movement (i.e. game protocols is a separation of concerns) for the players. Hence the game protocol language must guarantee that whenever a claim is true, the expression of winning strategy via the protocol language is possible, in other words, there exists a mapping SCG from claims to side-choosing games so that the side-choosing game for a given claim $\langle \Phi, A\rangle$ is a game played by a run-time proponent x and a run-time opponent y, denoted $SCG(\langle \Phi, A\rangle, x, y)$, such that there exists a winning strategy for participant x defending claim φ, given structure A (denoted as $ A |= \Phi $). Obviously, for standard semantic games, the protocol language always guarantees this. see Figure \ref{fig:standSCG}).

\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{standSCG.png}
\caption{\label{fig:standSCG} Standard semantic game, where ver = Proponent
 and fal = Opponent}
\end{figure}


Next, for illustrating purpose, we offer two simple examples of side-choosing games. In the first one we use Chess as reference game and in the second we use the semantic game behind a logical formula
as the reference game.

\begin{itemize}
\item{{\bf Chess game: Mate in 2}}\\
We start with a chess position similar to one chosen from Figure \ref{fig:checkmate}. And one player, the Proponent, claims to mate in 2 and the other, the Opponent, claims to prevent a mate in two. To determine the game outcome,
the players play from the given position to support their claim.

\begin{figure}[H]
\centering
\includegraphics[width=0.5\textwidth]{checkmatepuzzel.png}
\caption{\label{fig:checkmate}a checkmate puzzle from http://www.chess.com}
\end{figure}

\item{{\bf Semantic game: Saddle Point}}\\
In the second example, we use the logical formula: 
\[ \forall x \in [0,1] \exists y \in [0,1]: x\cdot y + (1-x)\cdot (1-y^2) \ge c \label{GM}\]
for some $c \in [0,1]$, e.g., $c = 0.615$. Behind every formula in predicate logic there is a semantic game between two players, one playing the Proponent role
and the other the Opponent role. The Opponent chooses the $\forall$ quantifier values and the Proponent the $\exists$ quantifier values.
The Proponent wins if the atomic formula to the right of : is true after the quantified variables have been assigned. The above sentence for
$c=0.615$ is true and therefore the Proponent has a winning strategy,
for example by using the Skolem function $y=x$.
\end{itemize}





\subsection{Algorithms to Analyze}

$\le_{WC}$ is {\bf defined} as:
$x \le_{WC} y $ if $wins(x) \ge wins(y)$.

$\le_{FC}$ is {\bf defined} as:
$x \le_{FC} y$ if $faults(x) \le faults(y)$.

We want to know whether the algorithms $\le_{WC}$ and $\le_{FC}$ 
are collusion-resilient.

%It is unacceptable  for a ranking function to reward losing
%or to penalize winning. 
%That is a player's rank cannot be worsened by an extra win
%nor can it be improved by an extra loss.
%
%If px <= py for table T then px <= py for table T' where
%T' contains an additional row where px won.
%We call this property Non-Negative Effect for Winning (NNEW.I).
%
%If px <= py for table T then px <= py for table T'' where
%T'' contains one fewer row where py won.
%We call this property Non-Negative Effect for Winning (NNEW.II).
%
%If px <= py for table T then px <= py for table T' where
%T' contains an additional row where py lost.
%We call this property Non-Positive Effect for Losing (NPEL.I).
%
%If px <= py for table T then px <= py for table T'' where
%T'' contains one fewer row where px lost.
%We call this property Non-Positive Effect for Losing (NPEL.II).


%The ranking functions property table:
%	NNEW.I	NNEW.II  NPEL.I NPEL.II 
%WC
%FC	TRUE	TRUE


%We say that a participant x controls a debate if x
%either wins or had a guaranteed opportunity to win (was non-forced).
%In a game there is at least one of the two participants
%in control: the winner.

\subsection{Property to Check}
{\bf Definition of collusion resilience}:
A ranking $\le$ of participants is said to be collusion-resilient
if for all debate tables $D$
and for any two participants $x$ and $y$, the property $x \le^{D} y$
implies $x \le^{E} y$, where $E$ is $D$ with added
debates $g$ that $x$ cannot control,
i.e., for which !g.control(x).

Informally, if $x \le^D y$ and more debates that $x$ cannot control
are added to $D$ resulting in $E$, then $x \le^E y$ holds.

%In other words, consider a table D defining a set of debates.
%If for any two participants x and y in table D,
%the property $x \le y$ holds for any table D'
%where D' contains an additional row
%for a debate that x cannot control.

\subsection{Choose your side and defend it}

\subsubsection{Question 1}
%{\bf Question 1.1}:
Is $\le_{WC}$ collusion resilient?

%{\bf Question 1.2}: 
\subsubsection{Question 2}
Is $\le_{FC}$ collusion resilient?

Justify your answer by providing a proof why the 
algorithm has the property or not.

Hint:
If you look for a positive answer, the proof is rather short.
If you look for a negative answer, it is enough to consider a small number of
participants only.

\subsection{Ranking Functions}
\section{The Challenge of Confusion}
A tournament can exhibit confusing behavior which makes it difficult to extract the most meritorious player.
The following confusing behaviors all may be present in a tournament.
In general, we don’t know whether a claim is true or false.
\begin{itemize}
\item
the correct side may be chosen, yet the defense will fail or, the incorrect side may be chosen, yet the defense will succeed.
In other words: true claims may be refuted and  false claims may be defended.
\item
players may lie about their strength and lose on purpose to help their colluding partner. 
\end{itemize}
The challenge is how to find order among all those confusing events.

An issue related to confusion is the garbage-in garbage-out property of SCG tournaments. If all players are weak, we cannot expect a useful outcome.


\section{Informal Reasoning about Ranking Mechanisms}
Before we give a formal proof why it is best to minimize unforced losses to securely rank players, we give a heuristic argument. Consider Table
\ref{tab:widgets} which defines 4 counting functions for SCG-tables:
For a player p: WF(p),WU(p), LF(p) and LU(p).
Let's analyze those 4 basic functions:
\begin{itemize}
\item
  {WF.}
Winning in forced side is an achievement but the loser could have lied about his/her strength and lost intentionally to benefit the winner. Therefore, WF could be abused and maximizing WF is not a reliable indicator of strength.
\item{WU.} Winning in unforced side is an achievement but the same argument as for WF applies. In addition, the loser could be forced in which case winning in unforced side is not a sign of strength. Therefore maximizing WU is not a reliable indicator of strength.
\item{LF.}
When you lose while forced you cannot be blamed. If your side choice was correct, it is expected that you lose unless the opponent is weak.
Therefore, LF is not an indicator of weakness and minimizing LF is not a reliable indicator of strength.

\item{LU (Fault).} Losing in unforced side is clearly a mistake. The loser got into a contradiction independent of whether the loser is proponent or opponent. Therefore, minimizing LU is a reliable indicator of strength.
\end{itemize}

The above argument is imprecise but gives a first hint why counting unforced losses is the best approach.

We now turn to two formal approaches to prove that fault counting
plays a central role. The first approach uses reasoning about monotonicity
constraints of functions and the second approach from \cite{Ahmed}
is using case analysis of a Venn diagram showing all possible
game outcomes for two players.

\section{Reasoning about ranking mechanisms via a general form scoring function}

% We use capital caligraphic latin letters to denote sets of all 

% modifiers
\newcommand{\const}[1]{\mathbf{#1}}
\newcommand{\faultRestrict}[2]{\restrict{#1}{fl}{#2}}
\newcommand{\controlRestrict}[2]{\restrict{#1}{c}{#2}}
\newcommand{\winRestrict}[2]{\restrict{#1}{w}{#2}}
\newcommand{\lossRestrict}[2]{\restrict{#1}{l}{#2}}

\newcommand{\faultRestrictComplement}[2]{\restrict{#1}{!fl}{#2}}
\newcommand{\controlRestrictComplement}[2]{\restrict{#1}{!c}{#2}}
\newcommand{\winRestrictComplement}[2]{\restrict{#1}{!w}{#2}}
\newcommand{\lossRestrictComplement}[2]{\restrict{#1}{!l}{#2}}

% Base Notation
\newcommand{\p}[1]{p_{#1}} % A player
\newcommand{\Ps}{P} % All players
\newcommand{\beats}[2][\p{}]{b^{#1}_{#2}} % a beating function
\newcommand{\allBeats}[2][\Ps]{B^{#1}_{#2}} % all beating function
\newcommand{\rank}[1]{\preceq_{#1}} % A ranking function
\newcommand{\order}[2]{\rank{#1}\!\!\!(#2)\:} % Applying a ranking function to a beating function
\newcommand{\allOrders}[1][P]{R^{#1}}
\newcommand{\faults}[2]{faults^{#1}(#2)}

% helpers
\newcommand{\opair}[2]{\langle #1 , #2 \rangle}
\newcommand{\otriple}[3]{\langle #1, #2, #3 \rangle}
\newcommand{\setcomp}[2]{\{#1\:|\:#2\}}
\newcommand{\restrict}[3]{#1|^{#2}_{#3}}


\newcommand{\s}[1]{s_{#1}} % a side
\newcommand{\Ss}{\const{S}} %all sides

\newcommand{\ver}{\const{\s{v}}} %proponent side
\newcommand{\fal}{\const{\s{f}}} %opponent side
\newcommand{\swc}{\s{wc}} %winner chosen side
\newcommand{\slc}{\s{lc}} %loser chosen side
\newcommand{\sw}{\s{w}} %winner side

\newcommand{\pw}{\p{w}}
\newcommand{\pl}{\p{l}}
\newcommand{\px}{\p{x}}
\newcommand{\py}{\p{y}}
\newcommand{\pz}{\p{z}}

Inspired by the utility theory from Artificial Intelligent,  we assigned each palyer a score, which comes from a uniformed utility function, or scoring function. Notice that all the infomation comes form the raw competition result table, and they can be classified into different cases (as shown in Figure \ref{fig:venn}). We find the less general proof using structured ranking based
on scoring easier and more revealing.

\begin{figure}[H]
\centering
\includegraphics[width=0.45\textwidth]{VennAllGame.png}
\caption{\label{fig:venn}Venn diagram for all possible game classification in terms of player x and y.}
\end{figure}

\begin{table}[H]
\centering
\large{
\begin{tabular}{c|c|c}
Winner & Loser & Forced\\\hline
$\px$ & $\py$ & None\\
$\px$ & $\py$ & $\py$\\
$\py$ & $\px$ & $\py$\\
$\px$ & $\pz$ & $\px$\\ 
\end{tabular}
}
\caption{\label A snippet of debate results table.}
\end{table}
\begin{table}[H]
\centering
\large{
\begin{tabular}{c|c|c}
Case & Win/Lose & Forced/Unforced\\\hline
WF & Win & Forced\\
WU & Win & Unforced\\
LF & Lose & Forced\\
LU(Fault) & Lose & Unforced\\ 
NP & Not participated & Not participated\\
\end{tabular}
}
\caption{\label{tab:widgets}It can be shown that for every debator, there are only 5 cases in each debate.}
\end{table}

Therefore, given a results table $T$ and a specified individual($\px$), there are actully 5 kinds of basic statistic infomation could be retrieved, i.e. 
$$WF(\px),\ WU(\px),\ LF(\px),\ LU(\px)\ and\ NP(\px)$$
Based on those infomation, one can define a ranking function:
$$U_{\px}=U(WF(\px),WU(\px),LF(\px),LU(\px),NP(\px))$$
\begin{comment}
$$U_{\px}=a_{1}WF(\px)+a_{2}WU(\px)+a_{3}LF(\px)+a_{4}LU(\px)+a_{5}NP(\px)$$
\end{comment}
Notice that, given the total number $|T|$ of games in the result table, we have:
$$NP(\px)=|T|-WF(\px)-WU(\px)-LF(\px)-LU(\px)$$
Therefore $U_{\px}$ can be rewriten as:
$$U_{\px}^T=U(WF(\px),WU(\px),LF(\px),LU(\px),|T|)$$
\begin{comment}
$$U_{\px}^T=a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}T$$
\end{comment}

And we should also specify that: $\px$ is weakly better than $\py$ under table $T$ iff $U_{\px}^T \le U_{\py}^T$. Then we could reform the $NNEW$, $NPEL$ and $CR$ ranking axioms in terms of scoring function as following:
\newtheorem*{NNEW_S}{NNEW}
\begin{NNEW_S}
\label{def:NNEW_S}
For any two players $\px$ and $\py$, given a table T, if T' comes from one more game, where $\px$'s won, added into T, then we have:
$U_{\px}^T \le U_{\py}^T \Rightarrow U_{\px}^{T'} \le U_{\py}^{T'}$
\end{NNEW_S}
\newtheorem*{NPEL_S}{NPEL}
\begin{NPEL_S}
\label{def:NPEL_S}
For any two players $\px$ and $\py$, given a table T, if T' comes from one more game, where $\py$'s lost, added into T, then we have:
$U_{\px}^T \le U_{\py}^T \Rightarrow U_{\px}^{T'} \le U_{\py}^{T'}$
\end{NPEL_S}
\newtheorem*{CR_S}{CR}
\begin{CR_S}
\label{def:CR_S}
For any two players $\px$ and $\py$, given a table T, if T' comes from one more game, where $\px$'s out of control (which means either $\px$ has not participated or $\px$ was forced to lose), added into T, then we have:
$U_{\px}^T \le U_{\py}^T \Rightarrow U_{\px}^{T'} \le U_{\py}^{T'}$
\end{CR_S}

For convenience of analysis, certain monotonicity notations should be introduced (Notice that we're just borrowing differential notations here, but,  in fact, since function $U$ is discrete, it cannot be differentiated):
\begin{equation*}
\begin{aligned}
&\partial_{X} U \ge 0\ \text{: U is monotonically non-decreasing on X}\\
&\partial_{X} U \le 0\ \text{: U is monotonically non-increasing on X}\\
&\partial_{X} U = 0\ \text{: U is indifference on X}\\
&Where\ X\in \{WF,\ WU,\ LF,\ FU,\ |T|\}
\end{aligned}
\end{equation*}

Being provided with the definitions and notations above, one can start reason about the inner monotonical properties of the scoring function. Suppose we have a result table $T$, and from the table we have two players $\px$ and $\py$, where $U(\px) \le U(\py)$. And this inequality shall hold under $NNEW$, $NPEL$ and $CR$, which are the ranking axioms.

First, we can prove that the information of $|T|$ could be eliminated from the scoring function, if it's $CR$; Based on $CR$ axiom, we consider a special case in which we add more games to a given result table $T_0$ where neither $\px$ nor $\py$ have participated. That means, in this special case, one can regard the scoring function of $\px$ and $\py$ as a function of only one variable $|T|$: 
\begin{equation*}
\begin{aligned}
U_{\px}^{T}=U_{\px}^{T}(|T|)\\
U_{\py}^{T}=U_{\py}^{T}(|T|)
\end{aligned}
\end{equation*}
then we define a new comparison function: 
$$R_{xy}(|T|)=U_{\px}(|T|)-U_{\py}(|T|)$$
now suppose we have $U_{\px}(|T_0|)\le U_{\py}(|T_0|)$. Since $CR$ needs this inequality maintained unchanged during more games being added, in which both $\px$ and $\py$ are out of control, we have:
$$\partial_{|T|}R_{xy}(|T|) \le 0 \text{\ for\ } |T| \ge |T_0|$$
however one can also suppose that $U_{\px}(|T_0|)\ge U_{\py}(|T_0|)$. And based on $CR$ for this case, we have the contrary constraint:
$$\partial_{|T|}R_{xy}(|T|) \ge 0 \text{\ for\ } |T| \ge |T_0|$$
then one can obtain
\begin{equation}\label{m_lce_0}
\begin{aligned}
\partial_{|T|}R_{xy}(|T|) = \partial_{|T|}(U_{\px}^{T}-U_{\py}^{T}) = 0
\end{aligned}
\end{equation}
that means the effect of increasing the size of table is independent with the comparison of score between any two players. This property gives us a good reason to ignore the $|T|$ (as well as $NP$) in future analysis, which allows us to redefine the form of scoring function as:
$$U_{\px}^T=(WF(\px),WU(\px),LF(\px),LU(\px))$$

Next, we shall see a scoring function is $NNEW$, if and only if we add one more game, where $\px$ won and $\pz$ lose, to the result table $T$ to form a new table $T'$, and the inequality $U_{\px}^{T'} \le U_{\py}^{T'}$ unchanged, which means we have either:
\begin{comment}
\begin{equation*}
\begin{aligned}
&U_{\px}^{T'} \le U_{\py}^{T'}\\
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}T'\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}T'
\end{aligned}
\end{equation*}

that means either:
\end{comment}

\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px)+1,WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py),LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}[WF(\px)+1]+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px)+1,LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py),LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}[WU(\px)+1]+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}

Hence we know that:
\begin{equation*}
\begin{aligned}
a'_{1} \le 0\\
a'_{2} \le 0
\end{aligned}
\end{equation*}
\end{comment}
Hence we reform $NNEW$ in terms of the monotonicity of $U$:
\begin{equation}\label{m_nnrw}
\begin{aligned}
\partial_{WF} U \le 0\\
\partial_{WU} U \le 0
\end{aligned}
\end{equation}

Similarly, a scoring function is $NPEL$, if and only if we add one more game, where $\py$ lose and $\pz$ won, to the result table $T$ to form a new table $T'$, and the inequality $U_{\px}^{T'} \le U_{\py}^{T'}$ unchanged, which means we have either:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py)+1,LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}[LF(\py)+1]+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py),LU(\py)+1)
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}[LU(\py)+1]+a_{5}[T+1]
\end{aligned}
\end{equation*}
Hence we know that:
\begin{equation*}
\begin{aligned}
a'_{3} \ge 0\\
a'_{4} \ge 0
\end{aligned}
\end{equation*}
\end{comment}
Hence we reform $NPEL$ in terms of the monotonicity of $U$:
\begin{equation}\label{m_nprl}
\begin{aligned}
\partial_{LF} U \ge 0\\
\partial_{LU} U \ge 0
\end{aligned}
\end{equation}

Finally, we come again to analyze the axioms of $CR$. We shall see that a scoring function is CR if and only if the following two cases hold.

The first case: we add one more game, where $\px$ not participated, to the result table $T$ to form a new table $T'$, and to maintain the inequality $U_{\px}^{T'} \le U_{\py}^{T'}$ unchanged, we have 5 cases:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py)+1,WU(\py),LF(\py),LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}[WF(\py)+1]+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py)+1,LF(\py),LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}[WU(\py)+1]+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py)+1,LU(\py))
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}[LF(\py)+1]+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px),LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py),LU(\py)+1)
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}[LU(\py)+1]+a_{5}[T+1]
\end{aligned}
\end{equation*}
\end{comment}
or y also didn't participate in the added game, that means nothing will change.
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}LF(\px)+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
Hence we know that:
\begin{equation*}
\begin{aligned}
a'_{1} \ge 0,\ 
a'_{2} \ge 0\\
a'_{3} \ge 0,\ 
a'_{4} \ge 0
\end{aligned}
\end{equation*}
\end{comment}
 This gives us monotonicity constrains:
\begin{equation}\label{m_lce_1}
\begin{aligned}
\partial_{WF} U \ge 0,\ 
\partial_{WU} U \ge 0,\\
\partial_{LF} U \ge 0,\ 
\partial_{LU} U \ge 0
\end{aligned}
\end{equation}

The second case: we consider the case where $\px$ was forced to lose the game. We add one more game, where $\px$ forced to lose and either $\py$ or $\pz$ won the game, to the result table $T$ to form a new table $T'$, and to maintain the inequality $U_{\px}^{T'} \le U_{\py}^{T'}$ unchanged, we must have either:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px)+1,LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py)+1,LF(\py),LU(\py)+1)
\end{aligned}
\end{equation*}
or:
\begin{equation*}
\begin{aligned}
&U_{\px}^{T}(WF(\px),WU(\px),LF(\px)+1,LU(\px))\\
&\le U_{\py}^{T}(WF(\py),WU(\py),LF(\py),LU(\py)+1)
\end{aligned}
\end{equation*}
\begin{comment}
\begin{equation*}
\begin{aligned}
&a'_{1}WF(\px)+a'_{2}WU(\px)+a'_{3}[LF(\px)+1]+a'_{4}LU(\px)+a_{5}[T+1]\\
&\le a'_{1}WF(\py)+a'_{2}WU(\py)+a'_{3}LF(\py)+a'_{4}LU(\py)+a_{5}[T+1]
\end{aligned}
\end{equation*}
Hence we know that:
\begin{equation*}
\begin{aligned}
a'_{3} \le 0
\end{aligned}
\end{equation*}
\end{comment}
This gives us the monotonicity constrain:
\begin{equation}\label{m_lce_2}
\begin{aligned}
\partial_{LF} U \le 0
\end{aligned}
\end{equation}
Combining constrains of \ref{m_lce_2} with \ref{m_lce_1}, we have reformed CR in terms of the monotonicity of $U$:
\begin{equation}\label{m_lce}
\begin{aligned}
\partial_{WF} U \ge 0,\ 
\partial_{WU} U \ge 0 \\ 
\partial_{LF} U \ge 0,\ 
\partial_{LU} U = 0
\end{aligned}
\end{equation}

In summation, the analysis above is enough to determine the monotonicity of scoring function from ranking axioms, and we can reform the axioms with the monotocity of the scoring function as following:
\begin{equation*}
\begin{aligned}
NNEW :\ &\partial_{WF} U \le 0,\ \partial_{WU} U \le 0\\
NPEL :\ &\partial_{LF} U \ge 0,\ \partial_{LU} U \ge 0\\
CR :\ &\partial_{WF} U \ge 0,\ \partial_{WU} U \ge 0,\ \partial_{LF} U = 0,\\ 
&\partial_{LU} U \ge 0,\ \ \partial_{|T|}(U_{\px}^{T}-U_{\py}^{T}) = 0\\
\end{aligned}
\end{equation*}

And if we define a new property of Local Fault Based (LFB), which simply means that the comparison of scores between any two players only depend their fault counting, as the combination of constrains in \ref{m_lce_0}, \ref{m_lce} and \ref{m_nnrw}:
\newtheorem*{LFB_S}{LFB}
\begin{LFB_S}
\label{def:LFB_S}
\begin{equation*}
\begin{aligned}
\partial_{WF} U = 0 &,\ \partial_{WU} U = 0,\\ \partial_{LF} U = 0 &,\ 
\partial_{|T|}(U_{\px}^{T}-U_{\py}^{T}) = 0
\end{aligned}
\end{equation*}
\end{LFB_S}
Then we can easily derive the following relations among those axioms and the $LFB$ property:
\begin{equation*}
\begin{aligned}
\text{NNEW} \wedge \text{CR} &\Rightarrow \text{LFB} \\
\text{NPEL} \wedge \text{LFB} &\Rightarrow \text{CR} \\
\text{NNEW} \wedge \text{NPEL} &\Rightarrow (\text{CR} \Leftrightarrow \text{LFB})\\
\end{aligned}
\end{equation*}
In the next section, we shall see that these relations could be proved as a theorem via a more general ranking function definition.

\section{Reasoning about General Collusion-Resistant Ranking Functions}

We first define certain notations which will be used in the latter analysis:

\begin{definition}
$T$ is an SCG table with columns W,L and F and derived columns Fault and Control.
\end{definition}
\begin{definition}
$T_0$ is the empty SCG table.
\end{definition}
\begin{definition}
$T_0$ is the empty SCG table.
\end{definition}
\begin{definition}
$Win(p)$ is the winning filter for a SCG table given a specified player p. More specifically, $T\{Win(p)\}$ will return a sub-table of $T$, where column W contains only player $p$.
\end{definition}
\begin{definition}
$Lose(p)$ is the losing filter for a SCG table given a specified player p. More specifically, $T\{Lose(p)\}$ will return a sub-table of $T$, where column L contains only player $p$.
\end{definition}
\begin{definition}
$Fault(p)$ is the fault filter for a SCG table given a specified player p. More specifically, $T\{Fault(p)\}$ will return a sub-table of $T$, where column Fault contains only player $p$.
\end{definition}
\begin{definition}
$Control(p)$ is the Controlling filter for a SCG table given a specified player p. More specifically, $T\{Control(p)\}$ will return a sub-table of $T$, where column Control contains only player $p$.
\end{definition}
\begin{definition}
A ranking function $\rank{}$ is an order function between any two players, which takes in a SCG-table as input and returns an order relation between the two players. 
\end{definition}


We now give a representation theorem for collusion resilient ranking functions.
In essence, we show that under basic monotonical properties of ranking functions, the limited collusion effect property is logically equivalent to 
using a ranking function that is based on a generalized form of fault counting. 
% We start by formalizing our notion of generaliz
% 
% We now show that: in the context of ranking functions satisfying both NNEW and NPEL axioms, there is an equivalent, yet a more practical, alternative
% characterization of collusion resilient ranking functions. We start by formalizing the alternative axiom. Then we formally prove a theorem formalizing the
% relationship between the two characterizations.

A ranking function $\rank{}$ is said to be \textbf{Local Fault Based (LFB)} if for any two arbitrary players $\px$ and $\py$ the 
relative rank $\rank{}$ assigns to $\px$ with respect to $\py$ solely depends on the games where $\px$ or $\py$ make a fault. Formally, 
\[\px \order{}{T\{Fault(\px)\}+T\{Fault(\py)\}} \py \Leftrightarrow \px \order{}{T} \py \label{eqn:LFB}\]

\newtheorem{Theorem}{Theorem}

\begin{Theorem}
For any ranking function having NNEW and NPEL, CR is equivalent to LFB. Formally, NNEW $\wedge$ NPEL $\Rightarrow$ ( CR $\Leftrightarrow$ LFB ). 
\label{theorem:LFB}
\end{Theorem}

\begin{figure}[H]
\centering
\includegraphics[width=0.45\textwidth]{VennSimple.png}
\caption{\label{fig:venn_s}Simplified Venn diagram for all possible game classification in terms of player x and y.}
\end{figure}

Figure~\ref{fig:venn_s} presents a partitioning of the games represented by an arbitrary table $T$. 
This partitioning illustrates the intuition behind this theorem and its proof. The intuition is that a ranking function satisfying the LFB property $\rank{}$ must completely 
decide the relative rank of any two arbitrary players $\px$ and $\py$ based on the games in the partition 2,4,3,5 only. 
Games in the other partitions cannot influence the relative rank of $\px$ and $\py$ assigned by $\rank{}$. 

We now give a proof of this theorem using the partitioning shown in Figure~\ref{fig:venn_s}. Our theorem follows directly from both lemmas.
\newtheorem{Lemma}{Lemma}
\begin{Lemma}
NNEW $\wedge$ CR $\Rightarrow$ LFB.
\end{Lemma}
To prove the first lemma, let $\rank{}$ be a ranking function that violates the LFB property. 
By definition of the LFB property, there must be two players $\px$ and $\py$ such that the games in regions 2, 4, 3, 5 influence the relative rank assigned by $\rank{}$ to $\px$ and $\py$.
The influence can either be positive (case I) or negative (case II) for $\px$. 

Suppose that games in regions 1, 6, 7 positively influence the rank assigned by $\rank{}$ to $\px$ with 
respect to $\py$. But, assuming that $\rank{}$ satisfies the CR property, games in regions 1, 7 cannot improve $\px$'s rank with respect to $\py$ because it only contains games 
not under $\py$'s control. Also, assuming that $\rank{}$ satisfies the NNEW property, games in region 6 cannot improve $\px$'s rank with respect to $\py$ because it only contains games that 
$\py$ has won. Therefore, our assumption that $\rank{}$ satisfies both CR and NNEW cannot be true. We have shown the contrapositive for case I.

We now consider case II. Suppose that games in regions 1, 6, 7 negatively influence the rank assigned by $\rank{}$ to $\px$ with respect to $\py$. 
But assuming that $\rank{}$ satisfies the CR property, games in regions 6, 7 cannot worsen $\px$'s rank with respect to $\py$ because it only contains games 
not under $\px$'s control. Also, assuming that $\rank{}$ satisfies the NNEW property, games in region 1 cannot worsen $\px$'s rank with respect to $\py$ because it only contains games that 
$\px$ has won. Therefore, our assumption that $\rank{}$ satisfies both CR and NNEW cannot be true. We have shown the contrapositive for case II and the proof of Lemma 1 is now complete.
\begin{Lemma}
\label{LemmaNPEL-LFB-CR}
NPEL $\wedge$ LFB $\Rightarrow$ CR. 
\end{Lemma}
To prove the second lemma, let $\rank{}$ be a ranking function satisfying both NPEL and LFB. 
By definition of the LFB property, only games in regions 2, 4, 3, 5 influence the relative rank assigned by $\rank{}$ to $\px$ and $\py$.
Games in regions 2, 3 and 4 are under the control of $\px$. Only games in region 5 can influence the relative rank assigned by $\rank{}$ to $\px$ and $\py$, yet 
games in region 5 are not under the control of $\px$. However, games in region 5 are all faults made by $\py$ and by NPEL they cannot improve the rank of $\py$ with respect to $\px$. 
Therefore, only games under the control of $\px$ may worsen $\px$'s rank with respect to $\py$. A symmetric argument applies to the rank of $\py$. This completes the proof of Lemma \ref{LemmaNPEL-LFB-CR} and hence the theorem.

\begin{definition}
A player is perfect if it never makes a fault.
\end{definition}

Next we prove that a perfect player will be ranked at the top provided NNEW, NPEL and CR hold.


\begin{corollary}
All perfect players are ranked at the top given a ranking function which satisfies NNEW, NPEL and CR.
\end{corollary}
The proof follows directly from Theorem 1. We know that for a ranking function which is NNEW and NPEL, CR is equivalent with LFB. That means only fault counting will effect the ranking result. Also, we know that, a player can't improve his rank by losing a game, and a player can't decrease his rank by winning a game. That means only making a fault results in a lower rank. Hence all perfect players, who make no fault, shall be ranked at the top.

\section{Side-Choosing Games for Ranking Functions}

We argue in a later section that side-choosing games
are applicable in any formal science. The study of ranking
functions for side-choosing games is such a formal science.
We use semantic games, a special case of side-choosing games, to illustrate the self application.

$P$ is the set of participants.
\[\forall T \in {\rm SCG-Table}(P)~
\exists r \in {\rm Ranking}(P): r~{\rm satisfies}~{\rm NNEW, NPEL,CR} ~and
\]

\section{Specific Ranking Functions}
\subsection{Trivial ranking functions and Fault Counting Ranking Function }
We want to instantiate the general theory
with specific ranking functions. The simplest one is the trivial ranking function which assigns the same rank to all players. We shall see that the trivial ranking function satisfies NNEW, NPEL and CR.

The proof is simple, while NNEW, NPEL or CR all represented certain property that under some situations, the rank relation among the two specified players should not be effected, and since all players have been assigned the same rank, additional games won't effect the identity among the players. Therefore the trivial ranking function satisfies those properties.

\begin{definition}
A ranking function is a trivial ranking function $\preceq_0$, if and only if, for $\forall T$ and $\forall \px,\ \py$, it always have $\px\order{0}{T}\py$.
\end{definition}

Next we introduce the simplest nontrivial structured LFB ranking function: the Fault Counting Ranking Function 
$\rank{f}$. We shall see that this function also satisfies NNEW, NPEL and CR. First we introduce the fault counting function and fault counting ranking function:
\begin{definition}
A fault counting function $\faults{T}{\p{}}$ for a specified SCG-table T and player $p$ is defined as:
\[\faults{T}{\p{}} = |T\{Fault(\p{})\}| \label{eqn:faults}\]
\end{definition}
\begin{definition}
A fault counting ranking function $\preceq_f$ for a specified SCG-table T is defined as:
\[\px \order{f}{T} \py \Leftrightarrow \faults{T}{\px} \leq \faults{T}{\py} \label{eqn:faultcounting}\]
\end{definition}

The fault counting ranking function should be NNEW and NPEL. Since, intuitively, a win for participant $\px$ cannot be a fault and therefore cannot increase the number 
of faults $\px$ incurs and hence cannot worsen $\px$'s rank. A loss for participant $\px$ may be a fault if $\px$ was not forced. In this case, 
the fault count of $\px$ increases and consequently the rank of $\px$ may only worsen. A loss for participant $\px$ while $\px$ is forced would not be counted and the rank of $\px$ will not change.
\begin{Theorem}
$\rank{f}$ satisfies the NNEW and NPEL properties.
\label{theorem:FCHasNNRWAndNPRL}
\end{Theorem}
Furthermore, the fault counting ranking function satisfy CR property. The proof of Theorem~\ref{theorem:FCHasLCE} falls immediately from Theorem~\ref{theorem:LFB} and Lemma~\ref{lemma:FCHasLFB} which states that the fault counting ranking function has the LFB property.
\begin{Theorem}
$\rank{f}$ satisfies the LCE property.
\label{theorem:FCHasLCE}
\end{Theorem}
\begin{Lemma}
$\rank{f}$ satisfies the LFB property
\label{lemma:FCHasLFB}
\end{Lemma}

\begin{proof}
\begin{align*}
& \text{Consider the L.H.S of LFB applied to $\rank{f}$} \\
& \text{L.H.S.} = \px \order{f}{T\{Fault(\px)\}+T\{Fault(\py)\}} \py \\
& \text{By definition ~\ref{eqn:faultcounting}:} \\
& \Leftrightarrow \faults{T\{Fault(\px)\}+T\{Fault(\py)\}}{\px} \leq \faults{T\{Fault(\px)\}+T\{Fault(\py)\}}{\py} \\
& \text{By definition ~\ref{eqn:faults}:} \\
& \Leftrightarrow \faults{T}{\px} \leq \faults{T}{\py} \\
& \text{By definition ~\ref{eqn:faultcounting}:} \\
& \Leftrightarrow \px \order{f}{T} \py = R.H.S.\\
\end{align*}
\end{proof}

\subsection{Weighted Fault Counting Ranking Function}

Based on the simplest Fault Counting Function in the last section, we can further present a family of collusion-resistant ranking functions
which measure different kinds of weaknesses of the participants.

We consider positive weights assignment to fault classes where:
\begin{enumerate}
\item The winner is a forced opponent, weakness in proponent.
Weight = $\alpha$.
\item The winner is a forced proponent, weakness in opponent:
Weight = $\beta$.
\item The winner is a non-forced opponent, weakness in proponent:
Weight = $\gamma$
\item The winner is a non-forced proponent, weakness in opponent:
Weight = $\delta$
\end{enumerate}

Then we can define a serial of new filters for SCG-Table T in regards of those weights:
\begin{definition}
$Fault_\alpha(p)$ is the fault filter for a SCG table given a specified player p. More specifically, $T\{Fault(p)\}$ will return a sub-table of $T$, where column Fault contains only player $p$ who made fault in the first class.
\end{definition}
\begin{definition}
$Fault_\beta(p)$ is the fault filter for a SCG table given a specified player p. More specifically, $T\{Fault(p)\}$ will return a sub-table of $T$, where column Fault contains only player $p$ who made fault in the second class.
\end{definition}
\begin{definition}
$Fault_\gamma(p)$ is the fault filter for a SCG table given a specified player p. More specifically, $T\{Fault(p)\}$ will return a sub-table of $T$, where column Fault contains only player $p$ who made fault in the third class.
\end{definition}
\begin{definition}
$Fault_\delta(p)$ is the fault filter for a SCG table given a specified player p. More specifically, $T\{Fault(p)\}$ will return a sub-table of $T$, where column Fault contains only player $p$ who made fault in the fourth class.
\end{definition}

With definitions of those new filters, we can now give a definition of Weighted Fault Counting Ranking Function as following: 
\begin{definition}
A weighted fault counting function $faults_{\lambda}^{T}(\p{})$ for a specified SCG-table T and player $p$ is defined as:
\[faults_{\lambda}^{T}(\p{}) = \lambda|T\{Fault_\lambda(\p{})\}|,\ \lambda \in \{\alpha,\beta,\gamma,\delta\} \label{eqn:faults}\]
\end{definition}
\begin{definition}
A Weighted Fault Counting Ranking Function $\preceq_{w}$ for a specified SCG-table T is defined as:
\[\px \order{w}{T} \py \Leftrightarrow \sum_{\lambda \in\{\alpha,\beta,\gamma,\delta\}}faults_{\lambda}^{T}(\px) \leq \sum_{\lambda \in\{\alpha,\beta,\gamma,\delta\}}faults_{\lambda}^{T}(\py) \label{eqn:faultcounting}\]
\end{definition}

\[U(D) = \alpha \cdot \alpha Rows +
        \beta \cdot \beta Rows +
	\gamma \cdot \gamma Rows +
	\delta \cdot \delta Rows
\]

By suitably choosing the weights, we can influence
the competitiveness of the games. For example,
if $\beta = \gamma = \delta = 0$ and $\alpha>0$
there is less competition because three kinds
of weaknesses are not counted. And notice that once we assign identical value to all weights, the weighted fault counting function will degenerate to a simple fault counting function.

Following the proof of simple fault counting ranking function in the last section. It's easy to show that the weighted fault counting function is also NNEW, NPEL and CR.

\begin{comment}
Integrate this at the appropriate place:
We	 know	 that	any	 ranking	 function	 that satisfies	NNEW,	NPEL	and	
CR	is	in	the	form:

\[ U(x) = a LU(x), a \ge 0
\]

More	generally,	 $a$ could	even	be	a	non-negative	function	of	x,	i.e.,
\[ U(x) = a(x) LU(x), a(x) \ge 0
\]
\end{comment}

\section{Applications of Side-Choosing Games}

Our entry point to side-choosing games were semantic games
which have been studied by logicians for a long time [SEP].
Give definition.
Give simplified semantic games: one value for each 
quantified variable.

\subsection{Meritocracy Evaluation}
One important application for side-choosing games is meritocracy evaluation. Since we know that the less faults a player has made, the higher one should be ranked, so the one (we call such a player "quasi-perfect", because the claim he or she defended might actually be refuted by those who are stronger but not participated in the games) who made no faults should be top-ranked. Formally, we have the following theorem:

\newtheorem*{Meritocracy Theorem}{Meritocracy Theorem}
\begin{Meritocracy Theorem}
\label{def:Meritocracy Theorem}
NNEW and NPEL and CR imply that a quasi-perfect player is top-ranked, where the quasi-perfect player is a player who never makes a fault.
\end{Meritocracy Theorem}


\subsection{Teaching Formal Sciences}
Side-choosing games are attractive for teaching staffs
in formal sciences for the following reasons:

Students become active participants in teaching

students accept that when they make a fault there is
a problem in their argument: They chose a side but could not defend it. This holds independent of whether they chose the 
proponent or opponent role.

collaboration with a competitive flair

can use teaching environments like Piazza
(with disadvantage that all communications are open within each team). Use delayed publication.

\subsubsection{Teaching Algorithms}
\subsubsection{Teaching Software Development}
\subsection{Organizing Problem Solving Communities for Constructive Formal Sciences}
\subsubsection{Algorithm Development}
\subsubsection{Software Development}
\subsubsection{Robots}
\subsubsection{Dialog-Based Proofs}

\section{Future work}
\subsection{Extending SCG-Tables}
When more information is known about games and their results we can extend the SCG table. For example, the current SCG-table does not include information on whether the claim is true or false.
With this information added, we can consider new ranking functions.

From old paper

\section{Further Applications of Side-Choosing Games}
Wikipedia of Computations

OLD123
==============

We are after a ``Wikipedia of Computations'' where user's inventions are explicit 
and composable. A computation is specified by an interpreted predicate logic claim 
in a constructivist setting where computation is performed in
some computable model to refute the claim.
The claim is refuted when the semantic game associated with the claim is 
lost by the proponent. The semantic game takes place between the proponent
and opponent of the claim and requires the players to compute
objects that defend the players' positions of being proponent or opponent.
For the purpose of this paper we assume that the task of judging
claims as well as refuting them can be done by a software.
We have avatars playing the role of scholars who recognize true claims
and who know how to defend them. Those avatars have a simple interface
whose implementation defines an explicit invention which will be
judged against other inventions. 
%The inventions are composable 


Computations in the ``Wikipedia of Computations''
are queried by a predicate logic claim and either a
lab is found which solves that claim or a new lab is defined
to initiate a new call to the crowd to solve the claim.
Solving the claim means to provide the algorithms necessary to defend it.

What about the quality of the claims in the ``Wikipedia of Computations?''
That depends on the quality of the crowd participating in a specific lab.
If the crowd is strong and interested 
in the lab, the claims will resist refutation even under heavy attacks.
What about spammers trying to infiltrate a lab with false claims?
We have three precautions against spammers: (1) they have to defend 
their claims and (2) they don't know the identity of their adversary
(3) they are responsible for the positions they have taken and might have
to defend them against other stronger players.



\subsubsection{Software Development}

At first, it appears strange to have a crowd working on the implementation 
of a formally-specified function (one of the Skolem functions implied
by a claim). Why not just hire one good programmer? 
Isn't the good programmer distracted by having to write
an avatar to play semantic games?
The formally-specified function can often be implemented in many different ways
which have different qualities.
%used  by the objective function 
%in the claim.
To find the optimum quality may be challenging and competition
will improve the quality of the software.

It is true that in the end only one good programmer is needed
but the problem is how to find her or him.
A lab serves this purpose.

The avatar has a meta interface which consists of the following tasks:
\begin{enumerate}
  \item Choose a claim out of a set of claims.
  \item Take a position on a claim, either as proponent (if 
  the avatar thinks the claim is true) or opponent (if the avatar thinks the claim
  is false).
  \item Play the next move in the semantic game.
\end{enumerate}
Actual avatar interfaces are generated specific to each lab.

Our system uses a Crowd Interaction Mechanism (CIM) to make
``optimal'' use of the crowd. The CIM tries to create the most 
information out of the games that are played.
For example, if for a claim c there are 2 proponents v1,v2 and 2 opponents f1,f2,
the CIM will create 2 games: v1/f1 and v2/f2 and not two games v1/v2 and f1/f2.

Our system might appear expensive because users
don't see each others' software (unless there was a 
``level the boats'' event).
They have to try to reverse engineer the programs
of other users. We feel that this is the price to
pay for getting new ideas into the software.
We would not recommend our system for 
formally specified computational problems
where no innovation is expected to solve them effectively.

%global properties

% Example
% quantifiers for users, quantifiers for machine
% user quantifiers and machine quantifiers

As a running example, consider the $MinBasisSize$ problem:

\emph{Size of minimum graph basis}: a basis of a directed graph $G$ is defined as set of nodes such that
  any node in the graph is reachable from some node in the basis. Formally,
\[
    MinBasisSize(G \in Digraphs, n \in \mathbb{N}) = \]
\[    BasisSize(G, n) \wedge \forall k~s.t.~k < n : \neg BasisSize(G, k)
\]
where
      \[ BasisSize(G \in Digraphs, n \in \mathbb{N}) = \]
\[      \exists s \in \mathcal{P}(nodes(G))~s.t.~|s|=n~:\]
\[ \forall m \in nodes(G)~\exists p \in paths(G):\]
\[first(p) \in s \wedge last(p) = m.\]

In the following we assume that the reader is familiar with semantic games.
In appendix B there is a concise definition.

The software (avatar) we want to have developed takes a graph G and natural
number n and it will tell us whether it wants to be proponent 
or opponent. Let's assume, the avatar wants to be proponent
and the CIM has found another avatar who wants to be opponent.
Who is right? The semantic game between the two will give us further information:

There are two cases:
\begin{itemize}
\item {First conjunct}

If the opponent chooses the first conjunct: $BasisSize(G,n),$
she thinks that there is no vertex basis of size $n$ for $G$.
In this case, the proponent must provide a set $s$ of $n$ nodes 
and the opponent must provide a node $m$ and
the proponent must provide a path $p.$
If $ first(p) \in s \wedge last(p) = m $
the proponent wins, otherwise the opponent wins.

\item {Second conjunct}

Remember that negation means that the users switch roles proponent $\iff$ opponent.
If the opponent chooses 
the second conjunct: $\forall k~s.t.~k < n : \neg BasisSize(G, k),$
she thinks that she can strengthen $MinBasisSize(G,n)$ to a smaller $n.$
In this case, the opponent chooses a $k$
and a set $s$ of $k$ nodes 
and the proponent provides a node $m$ and 
the opponent provides a path $p.$
If $ first(p) \in s \wedge last(p) = m $
the opponent wins, otherwise the proponent wins.
\end{itemize}

The above claim $BasisSize(G,n)$ does not discriminate between 
``hard'' and ``easy'' quantifiers.
Indeed, the existential quantifier for $s$ seems harder
than the universal quantifier for $m$ and the existential quantifier for $p$.
We can take care of the last two quantifiers with
a predicate $reachAll(G,s)$ which checks, using DFS, whether we can reach 
all nodes in $G$ from $s.$
$reachAll(G,s)$ is implemented in the model of graphs. We now use this function,
reducing the communication needs between proponent and opponent:
\[ BasisSize(G \in Digraphs, n \in \mathbb{N}) =\]
\[ \exists s \in \mathcal{P}(nodes(G))~s.t.~|s|=n~: reachAll(G,s)\] 
%$ \forall m \in nodes(G)~\exists p \in paths(G): first(p) \in s \wedge last(p) = m $.

We see in this example that the lab designer has a choice how the 
avatars (or users, in general) are engaged. Notice that the 
reduction of quantifiers simplifies the semantic game.

We want to solve the $MinBasisSize(G,n)$ problem incrementally.
Let's first make the simplifying assumption that $G$ is a DAG (directed
acyclic graph).
It seems easier to solve the $MinBasisSize$ problem for this special class of graphs.
We have now a new lab where the claims are of the form:
\[
BasisSize(G \in DAGs, n \in \mathbb{N}) = \]
\[ \exists s \in \mathcal{P}(nodes(G))~s.t.~|s|=n~: reachAll(G,s).\]
Let's assume we have a solution for this lab. We are lucky to have 
now a solution for the general graphs because there exists
a mapping from general graphs to DAGs that preserves reachability.
A path in the original graph translates into a path (possibly of length 0)
in the DAG.
This results by itself in a lab for the transformation.
We have a graph $G_1=(V_1,E_1)$ and we construct a new DAG $G_2=(V_2,E_2)$ from $G_1.$
We claim there exists a mapping 
$f(G_1) \rightarrow G_2$ 
%and $f_E(G_1) -> E_2$
with two important properties:
(1) the 
{\bf defense (refutation) of claim} $BasisSize(G_2,n)$  
{\bf results in a defense (refutation) of claim} $BasisSize(G_1,n).$ 
(2) there is no information loss: 
%If in lab1 there is an instance 
$\forall G_1:$ if $BasisSize(G_1,n)$ then $BasisSize(f(G_1),n).$ 



% $f(G_1)$ induces a mapping $f$ from $V_1$ onto $V_2$ where $V_2$ is generally smaller
% than $V_1$.
% During the 
% %$BasisSize(G_1 \in DAGs, n \in \mathbb{N})  
% 

% \subsection{Computational Problems and Predicate Logic}
% Computational problems can be classified into decision, search, optimization, counting, and promise problems. 
% Predicates, such as $R(x,y)$, are used to denote decision problems, functions, such as $S(x)$, are used to denote 
% search problems. Search problems can be constructed from decision problems as $S(x) = \{y \mid R(x,y)\}$. Decision 
% problems can be seen as a search problem with a yes/no answer. Similarly, counting and optimization problems can be 
% constructed from decision problems and decision problems can be constructed back from them. Promise problems 
% generalize decision problems by restricting the inputs. Following a long tradition in computational complexity, we 
% take decision problems as the fundamental computational problem.
% 
% 
% Predicate logic statements can be used to specify composite predicates denoting decision problems. 
%  
% \subsection{Logical Games}
\subsection{Logical Games and Computational Problems}
Logical games have a long history going back to Socrates. More recently, they became a familiar tool in many branches 
of logic. Important examples are Semantic Games (SGs) used to define truth, back-and-forth games used to compare 
structures, and dialogue games to express (and perhaps explain) formal proofs~\cite{LogicalGames},~\cite{sep-logic-games},~\cite{sep-logic-dialogical}.


SGs are played between two players, the \emph{proponent} and the \emph{opponent}~\footnote{Other names has been also used in the literature such as \emph{I} and \emph{Nature}, \emph{Proponent} and \emph{Opponent}, and \emph{Alice} (female) and \emph{Bob} (male).}.
% Let L be a language of first-order logic. 
An instructive way of viewing SGs is in their extensive form, which essentially is a tree structure
with the root labeled by the formula $\phi$ 
%of L
, the subsequent labeled
nodes representing the subformulas of $\phi$, and the vertices labeled by
the actions of the players.


In the theory of SGs, logical statements interpreted in a computable model (a.k.a. claims) derive their
meaning from the games played by the rules prompted by the logical
connectives encountered in the claims~\cite{SGIntro}. 
% The game starts with the
% outermost component and proceeds systematically from outside in.
The existence of a winning strategy for the \emph{proponent} implies
that the underlying logical statement is indeed \emph{true} and the existence of a winning strategy for the \emph{opponent} 
implies that the underlying logical statement is indeed \emph{false}. 


Players need to solve \emph{computational problems} in the course of playing SGs. For example, the opponent of the 
$prime(7) = \forall k\ s.t.\ 1 < k < 7: \neg divides(k,7)$ needs to compute the factors of $7$. 
Similarly, claims can be used to logically specify computational problems. For example, consider the problem of finding the factors of a given 
natural number $factors(n)$. This problem can be logically specified using the claim 
$\forall n \exists s : \forall k : divides(k,n) \Leftrightarrow k \in s$. In SGs derived from this claim, the proponent needs to correctly 
solve $factors(n)$ in order to win.

A computational problem can be logically specified as a claim about the relation between either
(1) the input properties and the output properties, or 
(2) the input properties and the output finding process properties such as resource consumption.


\section{Thesis}
Our thesis is that semantic games of interpreted logic statements provide a useful foundation for building 
\emph{successful} crowdsourcing systems for solving computational problems.

\subsection{Rationale and Limitations of Semantic Games}
SGs of claims provide attractive answers to the four challenging questions of crowdsourcing systems.
However, these answers are only valid in a limited context. A \emph{successful} SG-based system must generalize SGs 
to a much wider context and improve on the way SGs address these four challenging questions, whenever possible.

 An example of such limitation is that SGs define an interaction mechanism between two users only. A successful SG-based 
 crowdsourcing system must provide a Crowd Interaction Mechanism (CIM) on top of SGs that decides which SGs to be played. To decide on 
 a game to be played, the CIM must decide on a claim, a user to take on the proponent position and a user to take on the opponent position. 
 On one hand it is important that the CIM relies on user preferences to enhance the user experience, ensure that user contributions are potentially 
 correct, and to ensure the fairness of SG-based evaluation. 
 On the other hand, the overall system would be ineffective if the CIM was just a proxy to users' preferences because the CIM 
 would no longer be able to \emph{drive} the user interaction. For example, it would be impossible to hold an 
 SG between two arbitrary users unless they hold contradictory positions on the same claim. 
 
\subsubsection{User Contributions}
During the course of playing an SG, users make two kinds of \emph{formal} contributions: positions and supporting actions.
These two kinds of contributions can be extracted from SG traces as follows:

The trace of an SG can be represented as a \emph{directed line graph} where nodes represent the state of the SG and edges represent transitions. 
The state is a tuple consisting of a claim and a pair of players, the player taking the proponent position and the player taking the opponent position. 
For example, the tuple $\langle c,p_1,p_2\rangle$ represents a state where $p_1$ is the player taking the proponent position and $p_2$ is the player taking the opponent position on claim $c$.
A labeled transition represents a supporting action while an unlabeled transition represents an implied action. 
Implied actions are automatically carried out by the system. An example of implied actions is given by: $\langle \neg c,p_1,p_2\rangle \xrightarrow{} \langle c,p_2,p_1\rangle$.
Supporting actions are either attacks or defenses, and they involve an additional parameter that one of the users must provide.
For example, the transition 
$\langle \forall x : p(x), p_1, p_2 \rangle \xrightarrow{x_0} \langle p(x_0), p_1, p_2 \rangle $ is an attack made by $p_2$, where $x_0$ is a counter example provided by $p_2$.
 
Apart from playing SGs, users can still contribute by improving their own SG playing strategies. 
Players, by improving their strategies, are able to spot 
more problems in the positions taken by their opponents in future games. 
Because users have to follow a well defined formal protocol~\ref{section:SGDef} to play an SG, 
this enables users to \emph{automate} the execution of their strategies into \emph{avatars}.
Algorithms used in avatars are themselves yet another potential formal contribution (see Section ~\ref{sec:Applications}).


\subsubsection{Evaluating Users}
SGs provide an \emph{objective} and \emph{self-sufficient} approach to assess the \emph{relative strength} of users. 
Simply put, the winner of an SG is considered \emph{stronger} than the loser.
This approach is fundamentally different from the current evaluation schemes used in crowdsourcing systems 
such as: gold standards, trusted workers and probabilistic oracles, and disagreement-based schemes~\cite{EvalutingCrowdWithConfidence}.

Disagreement-based schemes evaluate the \emph{absolute strength} of users based on how often the user's contribution is ``correct'' where a 
``Correct'' contribution is defined to be \emph{similar} to the ``majority vote''. 
SG-based evaluation is independent of the ``correctness'' of user contributions.
Instead SG-based evaluation can \emph{objectively} judge one contribution to be ``better'' than the other. 
It is worth noting that the ``better'' contribution is not always necessarily \emph{similar} to the ``majority vote''.

SG-based evaluation is said to be \emph{self-sufficient} because, unlike gold standard evaluation, 
it is not based on a set of pre-populated test cases. Instead, the two users test each other.

% An SG-based crowdsourcing system must somehow decide which SGs to be played. To do so, 
% the system must decide on a claim, a user to play the role of the proponent and a user to take the role of 
% the opponent. It is possible that a system can delegate some of these decisions to the users. The system 
% must also utilize the outcome of a large number of SGs to evaluate users' strength. 

It is important to evaluate users' strength based on their performance in a large number of SGs.
The na\"{i}ve approach of summing the number of SGs the user won is unlikely to be fair due to several concerns that give 
one group of players an advantage over another group of players. A comprehensive list of these concerns is given by:

%  For the evaluation to be fair, 
% it is necessary to ensure that users where equally advantaged in the set of SGs used for the evaluation. A comprehensive 
% list of situations that gives a group of users an advantage over another group is listed below:

\begin{enumerate}
%   \item If the claim or the position is forced on one of the players of an SG, then that player is at a disadvantage.
  \item Users can be at an advantage (or at a disadvantage) if 
  		they % the system chooses to force them to
  		participate in more SGs 
  		where they are at an advantage (or at a disadvantage). A player is at an advantage (or at a disadvantage) in an SG 
  		if either the claim \concern{1.a} or the position \concern{1.b} is only forced on their adversary (or only forced on them).
  \item Users can be at an advantage (or at a disadvantage) if 
  		they %the system chooses to forces them to 
  		participate in more (or fewer) 
  		than the average number of SGs played by their counterparts \concern{2}.
  \item Users can be at an advantage (or at a disadvantage) if 
  		they %the system chooses to force them to 
  		participate in more SGs 
  		against other weaker (or stronger) users \concern{3}.
  \item If a group of users can form a coalition with the goal of artificially increasing the strength of 
  		a particular user through losing against that user on purpose, 
		then the winning user is at an advantage \concern{4}. 
\end{enumerate}

As we mentioned before, it would not be effective to address the first concern by ensuring that, 
in every game, %the system only chooses SGs in 
%which 
neither of the players is at an advantage (or a disadvantage). Instead, the system has to adopt a non-local view on fairness 
and ensure that none of the players in the crowd is at an advantage (or a disadvantage) considering all played SGs.
% 
% One potential approach to address the first concern is to ensure that the system only chooses SGs in which neither of the players 
% is at a disadvantage. However, this approach is ineffective because it make it impossible to get two users to play an SG 
% because they have to hold two opposing positions on some claim that they independently come up with. Furthermore, it makes it harder 
% to spot users holding the correct position on a particular claim but for the wrong reason.
% 
The second and third concerns can be addressed through either restricting the algorithm by which the system decides which SGs 
to be played, or through a more sophisticated approach to assess the user strength, or through both approaches.  
Anonymity can be used to defend against the fourth concern. 
%Suspecious behavior patterns can be uncovered as well by analyzing the history.
  
% An SG-based crowdsourcing system must evaluate users' strength based on the outcomes of a large number of SGs. let 
% Given the history large number of SGs
% 
% However, SG-based evaluation is only meaningful when: 
% \begin{enumerate}
%   \item None of the users is at a disadvantage (i.e. the game is fair). 
%   		% Neither the claim nor a particular position is forced on any of the users.
%   \item The loser was incentivised to win the game. %One player might wan another player to win
% \end{enumerate}
% Unfortunately, SGs are, by definition, played between players holding contradictory positions on the same claim. Combining this condition 
% with the first condition of meaningfulness of SG-based evaluation can result in very few SGs being played, thus rendering the overall
% system ineffective.
% 
% 	Who decides that two particular players should participate in an SG come from?
% 	Who chooses the claim?
% 	Who chooses the positions of players?


% \begin{verbatim}
% ==== End =====
% \end{verbatim}
% 
% SGs provide a structured and objective approach to evaluate users participating in them. 
% The winner of an SG is considered \emph{relatively stronger} than the loser.
% SGs are said to be \emph{self-evaluating} because the evaluation is not based on a set of pre-populated test cases,
%  a reminiscent of the beat the machine approach in ~\cite{attenberg2011beat-ipeirotis}. 
% The two players test each other. The approach can be considered \emph{fair} to the player that has willfully chosen 
% their position (either as the proponent or as the opponent) on the underlying claim, provided that the claim was fairly 
% chosen, both players were given an equal amount of resources during the game play, and the loser was properly 
% incentivised to win the game.
% 
% In an SG-based crowdsourcing system, a large number of SGs are played over an extended period of time. A successful system 
% can leverage the results of all SGs to evaluate the strength of users more accurately as well as to evaluate other qualities  
% of the users and their contributions. We refer to the the set of evaluated qualities and their computation algorithms collectively 
% as the \emph{evaluation structure}.

\subsubsection{Evaluating User Contributions}
Based on the outcome of an SG, we cannot safely assume that certain contributions are ``correct''. 
Therefore, the best we can do is to judge certain user contributions to be \emph{potentially correct}. 
We consider contributions to be potentially correct if we have no reason to believe they are potentially incorrect. 


By definition, the contributions of an SG loser are ``Incorrect''. Other reasons to believe that certain contributions 
are potentially incorrect include:
% contributions are 
%  than the contributions of the loser. 
% However, we cannot consider the winner contributions as \emph{potentially correct} 
% unless:
\begin{enumerate}
  \item The position taken by the winner was forced \concern{5}.
  \item There is no mechanism to discourage ``cheating'' (i.e. \emph{knowingly} making ``incorrect'' contributions) either because 
  		their adversary is weak enough not to discover the ``cheat'', or to lose on purpose against their opponent \concern{6}.
\end{enumerate}
Anonymity can be used to discourage ``cheating''. It is also possible to hold the positions taken by users against 
themselves in future SGs. %KARL? previous sentence not clear.
 %   \item The loser was incentivised to win the game.
% 
%  and regard the contributions of the winner as ``accurate''.
% Unfortunately, there is nothing that prevens users from ``cheating'' (i.e. \emph{knowingly} making ``inaccurate'' contributions).
% % Since SG contributions of the winner of an SG 
% % Even in a fair SG, there is nothing that prevents users from ``cheating'' 
% % (i.e. \emph{knowingly} making ``incorrect'' contributions). 
% Especially, against a much weaker adversary. 
% Therefore, it is necessary to somehow discourage ``cheating'' in order to ensure that the winner's contributions are ``accurate''. 


%%% Move later
% Therefore, it is necessary to ensure that users are \emph{required} 
% to support their positions against an \emph{arbitrary} strong adversary. There are several approaches to ensure that strong players 
% do not ``cheat'' such as anonymity of adversaries and holding the positions taken by players against themselves in future games.
% % , and having players playing against a reference player.  

% In the presence of a large number of semantic games played over a large period of time. It is possible to evaluate user contributions 
% based on earlier user contributions. For example, contributing a position that opposes the crowd belief is a \emph{breakthrough} 
% and can be considered \emph{superior} to contributing a position that matches the crowd belief.

\subsubsection{Combining User Contributions}
It is possible to collect the potentially correct contributions of all winners of SGs into a contribution database. 
The \emph{crowd beliefs} about claims can be assessed from the contribution database. 
It is possible that ``incorrect'' contributions make it to the contribution database \concern{7}.
Therefore, it is necessary to have a periodic mechanism to clean the contribution database in order to enable more accurate 
assessment of the crowd beliefs.


Apart from estimating the crowd beliefs, SG losers get precise feedback on how they can improve their SG playing strategies.
Furthermore, users can then build on the crowd beliefs. For example, suppose that the winners were mostly taking the proponent position on 
the claim $\forall k : divides(k,3571) \Leftrightarrow k \in \{1,3571\}$, then this likely-to-be-true claim can be used as 
a test case for factorization algorithms. 

% The strength of SG-based evidence is proportional to the strength of the losing player.

% In certain circumestances, individual SGs can be taken as evidences of the truth or falsehood of their underlying claims.
% 
% p1 willingfully says true then fails to support it
% p1forced p2forced winner   evidence
%    f       f        p1       as p1
%    f       f        p2       as p2
%    f       t        p1
%    f       t        p2
%    t       f        p1
%    t       f        p2
%    t       t        p1
%    t       t        p2

\subsubsection{Recruiting and Retaining Users}
Participating in an SG can provide users with an intrinsically rewarding experience. 
The exact intrinsic rewarding experience is user dependent. 
For example, some participants can find the act of game play against an adversary to be fun.
Others can enjoy the educational (or collaborative) nature of SGs that comes from the fact that the winner of 
an SG gives the loser very targeted feedback.

We believe that the following three factors could enhance the intrinsically rewarding experience that SGs provide to 
users:
\begin{enumerate}
  \item Choosing claims that both players find interesting \concern{8}.
  \item Allowing users to choose their positions on claims \concern{9}.
  \item Matching players with similar levels of strength \concern{10}.
\end{enumerate} 

Neither intrinsic nor extrinsic reward is absolutely superior
		\footnote{
		For example, consider using Amazon Mechanical Turk (AMT) to label all images indexed by Google. 
		Would that be as cost effective as the ESP game? 
		A second example is building the Wikipedia. Would it be as cost effective to build the Wikipedia using AMT?}
		\footnote{
		Extrinsic reward is believed to be superior in motivating automatic (motor) tasks, 
		while intrinsic value would be superior in motivating intelligent (cognitive) tasks ~\cite{pink2011drive},~\cite{thinkingFastAndSlow},~\cite{Ipeirotis:2011:Mice}.}.
However, most certainly, a crowd would have users that prefer both kinds of rewards. Therefore, it is still useful to 
include other encouragement and retention schemes \concern{11} such as instant gratification, providing ways to establish, measure, and show 
different qualities of the users, establishing competitions and providing ownership situations~\cite{CrowdsourcingSystemsOnTheWWW}.

% \begin{verbatim}
% ===== End =====
% \end{verbatim} 
% 
% The rationale is that: 
% \begin{enumerate}
%   \item IPLSs provide a language for users to concisely and precisely express decision problems, which is an important type
%   of computational problems. 
% %   		Other types of computational problems such as search, optimization and promise problems can be derived 
% %   		from decision problems. 
% % %   		Precise disputable claims are the building blocks for constructing formal scientific knowledge bases.
% % %   		SGs provide a structured approach for users to further contribute to formal scientific knowledge bases 
% % %   		through constructively arguing the correctness of claims.
% % %   		\footnote{
% % %   			In his book, ``Conjectures and Refutations'', Karl Popper, the prominent science philosopher of the 20th century,
% % % 			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.}
% %   %\item IPLSs and SGs address the first challenge by providing a structured approach for users to contribute to the construction of scientific knowledge bases.
%   \item SGs provide a structured, objective and constructive approach for users to dispute the truthfulness of IPLSs. 
%    Hence, SGs address both the second and the third challenges by providing a fair, objective, and open \footnote{In the sense that it is not limited to a fixed set of test cases.}
%    approach to assess both the strength of users as well as the truthfulness of a particular IPLS.
%   %, provided the two users participating in the semantic game of that IPLSs hold contradictory positions.
%   \item SGs address the user retention challenge by providing them with intrinsically rewarding experience 
% 		\footnote{
% 		Neither intrinsic nor extrinsic reward is absolutely superior.
% 		Extrinsic value would be superior in motivating tasks that require motor skills, while intrinsic value would be superior in motivating tasks that require cognitive skills ~\cite{pink2011drive}.
% 		For example, consider using Amazon Mechanical Turk (AMT) to label all images indexed by Google. 
% 		Would that be as cost effective as the ESP game? 
% 		A second example is building the Wikipedia. Would it be as cost effective to build the Wikipedia using AMT?}
% 		\footnote{ 
% 		The exact intrinsic rewarding experience is user dependent. 
% 		For example, the participant losing a SG might appreciate the targeted feedback (s)he receives.
% 		Other participants might just appreciate the interaction with (or the fight against) another user.}.
%   \item Predicate logic is a well established and widely applicable.% formal knowledge representation approach. 
% \end{enumerate}
% 
% By their definition, an SG is a two-person zero-sum game played between two players, called the proponent and the opponent, 
% holding contradictory positions on some interpreted logical statement \code{s}. Furthermore, if the proponent wins an SG, this does not 
% mean that \code{s} is \code{true}. It could also mean that the proponent is much stronger than the opponent. Also, a game 
% against a much weaker opponent might not be an intrinsically rewarding experience. Similarly, playing an SG derived from
%  logical a statement that is interpreted in a domain that is not of interest might not be a rewarding experience.
%  
% A \emph{successful} system would encourage players to participating in SGs. 
% 1. assign users to SGs that they find interesting.
% 2. assess users contributions and reward them accordingly.
% 3. Provide meaningful feedback.
% 
% Furthermore, a \emph{successful} system would encourage users to submit IPLSs for evaluation by correctly evaluate IPLSs 
% with high confidence: 
% 1. force users to be reliable.
% 2. Allocating users to interesting games and correctly combining their contribution.  
%  
% Finally, the system should be user friendly.
% 
% \begin{verbatim}
% ===== End =====
% \end{verbatim} 
% We call our system successful if it encourages users to submit IPLSs as well as to participate in SGs. 
% 
% User friendly 
% effectively combine SG results
% Fairly assess users contributions.
% 
% 
% By having a crowd of users playing
% 
% We call our system successful if it is effective in :
% \begin{enumerate}
%   \item assigning SGs to the crowd.
%   \item combining the results of SGs to 
%   \begin{enumerate}
%     \item correctly solve computational problems with high confidence.
%     \item accurately assess the users and their contributions.
%   \end{enumerate}
%   \item it can properly evaluate users and their contribution.
%   \item the increase in the users and their contributions would make the system more attractive.
%   \item it is user friendly. 
% \end{enumerate}
% 
% A \emph{successful} crowdsourcing systems for constructing formal scientific knowledge bases would \emph{encourage} 
% users to submit IPLSs. Two important  
% A good user interface
% 
% * good user interface.
% * good truthfulness assessment.
% 
% It is possible to collect a large number of IPLSs with the help of a crowd of users. However, it is not obvious how to
% assign SGs to users such that it is possible to:
% \begin{enumerate}
%   \item meaningfully evaluate users and their contributions based on several SGs,
%   \item provide more intrinsically rewarding experience to users.
% \end{enumerate}
% 
% so that their outcome can be combined in a meaningful way.
% 
% Despite the aforementioned attractive properties of SGs, they are by definition limited to two-person games between two
% players holding contradictory positions on a particular IPLS. Our challenge is to utilize 
% 
% 
% The challenge is to scale semantic games to multiple players and improve user retention.
% 
% \begin{verbatim}
% =========Start=========
% \end{verbatim}

\subsection{Applications}
\label{sec:Applications}
In this paper we use
an SG-based system for crowdsourcing computational problem solving.
However, there are several other significant applications
to teaching, crowdsourcing software development and crowdsourcing formal science.
%Besides using an SG-based crowdsourcing system for solving computational problems, it is also possible to 
%use it to for teaching, software development and formal science.

\subsubsection{Teaching}
The collaborative and self-evaluating nature of SGs is useful in teaching (especially MOOCs) where 
teaching other students helps boost one's evaluation.
The winner against a non-forced opponent teaches the opponent a lesson.

\subsubsection{Software Development}
The mandatory use of formal specification of claims and the orderly nature of the semantic games 
enables the system to be used as a crowdsourcing system for algorithms for computational problems as well. Because 
users can ``automate themselves'' as avatars (programs). The strongest avatars would have good algorithms either for 
generating tests for other avatars or solving a computational problem or both.

\subsubsection{Formal Science}
Although scientists in formal sciences are often interested in finding proofs to their claims, 
it remains helpful to test those claims first with the help of the crowd. Testing can provide them with 
useful insights. For example, testing can reveal a corner case where the claim does not hold. Reformulating 
the original claim to avoid such corner cases could be helpful in finding proofs~\cite{polymath}. It is worth mentioning that 
the phrase ``formal science'' is not limited to mathematics and logic. It also applies to scientific uses of formal simulation models.


% \subsection{Problem Formulation}
% To develop an SG-based crowd interaction mechanism that:
% \begin{enumerate}
%   \item provides a meaningful evaluation of users' strength.
%   \item provides a meaningful assessment of the crowd beliefs,
%   \item is effective,
%   \item is as intrinsically rewarding as possible.
% \end{enumerate}

\section{Initial Investigation}
To support our thesis, we designed and partially implemented~\cite{CurrentImpl} a proof of concept SG-based crowdsourcing system. 
Our system constitutes a redesign from scratch of the Scientific Community Game (SCG)~\cite{fscp-ws},~\cite{scg-def},~\cite{scg-bionetics} 
which has been evolving since 2007. Below, we describe our newly designed system and report on our experience of using earlier 
iterations of SCG for teaching.
%  Scientific Community Game (SCG) for teaching. 
% SCG is a predecessor of our current system that we implemented and tested. Further details about SCG and its evolution 
% can be found in ~\cite{fscp-ws},~\cite{scg-def},~\cite{scg-bionetics}.
% 
% To support our thesis, we designed and partially implemented~\cite{CurrentImpl} a proof of concept SG-based crowdsourcing system.
% Below, we describe our system and report on our experience of using the Scientific Community Game (SCG) for teaching. 
% SCG is a predecessor of our current system that we implemented and tested. Further details about SCG and its evolution 
% can be found in ~\cite{fscp-ws},~\cite{scg-def},~\cite{scg-bionetics}.

% To support our thesis, we designed and implemented a proof of concept SG-based crowdsourcing system with 
% three core components. We have also studied the necessary mechanisms that to be added to our current system. 
% Below, we briefly describe the system, the three core components, the necessary interaction mechanisms, and 
% report on our experience of using the Scientific Community Game (SCG) for teaching. 
% SCG is a predecessor of the SG-based crowdsourcing system we are developing. 
% Further details about SCG and its evolution can be found in ~\cite{fscp-ws},~\cite{scg-def},~\cite{scg-bionetics}.

% In a nutshell, our system uses first order logic for claims and uses the semantic games defined by 
% Hintikka's Game-Theoretic-Semantics~\cite{GTS-Hintikka}. Our system, uses \emph{labs} to define special interest groups 
% of users. A lab is created by an owner (one kind of users) and consists of a family of claims and a number of scholars 
% (another kind of users) that are \emph{interested} in evaluating these claims. Rather than participating in SGs directly, 
% scholars participate in Contradiction-Agreement Games (CAGs). CAG is a mechanism built on top of SGs and it can be used to 
% fairly evaluate scholar strength and enable them to meaningfully contribute to the crowd belief without the requirement that scholars 
% must be freely chosing opposite positions. Our system relies on anonymity to discourage scholars from knowingly making ``incorrect'' 
% contributions. 
% 
% Evaluation Algo, crowd belief. 
% 
% 
% 
% 
% 
% 
% our system relies on anonymity / and competitions.
\subsection{System Overview}
In a nutshell, our system uses first-order logic to express claim families (See Appendix~\ref{section:ClaimLang} for more details), 
and uses the semantic games of first-order logic formulas defined by Hintikka's Game-Theoretic-Semantics~\cite{GTS-Hintikka} 
(See Appendix~\ref{section:SGDef} for more details). 

To ensure that claims are never forced on users, our system uses labs. Labs define special interest groups of users. 
A lab is created by an owner (one kind of users) and consists of a family of claims. 
Scholars (another kind of user) choose to join the labs they find \emph{interesting}. The system only allocates users to 
SGs of claims from the labs they joined. This enhances the users' experience while participating in SGs \concern{8} and guarantees that users 
are never at a disadvantage regardless of the method used to chose the underlying claims for SGs \concern{1.a}.

% The main interaction mechanism of scholars with the system is called the \emph{driver} mechanism. The driver mechanism decides on 
% the SGs to be played, the scholars participating in every SG as well as their roles. However, 
Rather than making scholars participate in SGs directly, 
the CIM in our system makes users participate in Contradiction-Agreement Games (CAGs). Although CAGs are composed of SGs, 
CAGs can be played by two players taking the same position on the underlying claims. This enhances the users' experience \concern{9}. 
Furthermore, CAGs are specifically designed to provide a fair evaluation \concern{1.b} and to identify potentially correct contributions \concern{5}. 
CAGs are described in Section~\ref{sec:CAG}. Currently, our system has a per-lab CIM. Lab owners are required to provide their CIM 
mechanisms, e.g., to match scholars with close enough strength. This is critical to enhance the users' experience \concern{10} and 
fairness \concern{3}.

Our system uses an algorithm to evaluate the users' strength as fairly as possible. Our algorithm is designed to address the 
fairness concerns \concern{2,3}. The algorithm is described in Section~\ref{sec:userStrength}. 
To estimate crowd beliefs, our system uses a simple formula that is presented in Section~\ref{sec:crowdbeliefs}.
To discourage ``cheating'' \concern{4,6}, our system relies on anonymity. Currently, our system does not provide a mechanism for 
cleaning the contributions database \concern{7} nor any encouragement and retention schemes \concern{11} 
other than the fun that scholars get from participating in SGs.



% 
% Currently, our system delegates the implementation 
% of the driver mechanism to lab owners. However, there is
% 
% Mechanism restriction for 3, 10 
% 
% CAG for 1.b , 5, 9
% 
% Eval algo for 2, 3
% 
% To discourage ``cheating'' \concern{4,6}, our system relies on anonymity.
% 
% Cleaning mechanism for 7
% 
% E&R schems for 11
% 
%  
% \begin{enumerate}
%   \item It uses first order logic for expressing claims.
%   \item Interactions are based on the semantic games of first order logic formulas defined by 
%   		Hintikka's Game-Theoretic-Semantics~\cite{GTS-Hintikka}.
%   \item Rather than participating in SGs directly, scholars participate in Contradiction-Agreement Games (CAGs). 
%   		CAG is a mechanism built on top of SGs and it can be used to meaningfully evaluate user strength and enable users 
%   		to meaningfully contribute to the crowd belief without the requirement that users must have contradictory 
%   		positions on the underlying claim.
%   \item It provides algorithms to estimate user strength and crowd beliefs based on the outcome of several CAGs.  
%   \item It uses \emph{labs} to define special interest groups of users. A lab is created by an owner (one kind of users) and 
%   		consists of a family of claims and a number of scholars (another kind of users) that are \emph{interested} in 
%   		studying these claims.
%   \item It relies on anonymity to discourage ``cheating''.
%   \item It leaves the exact lab interaction mechanism for lab owners to design.
% \end{enumerate}
% 
% 
% In a nutshell, our system can be characterized as:
% \begin{enumerate}
%   \item It uses first order logic for expressing claims.
%   \item Interactions are based on the semantic games of first order logic formulas defined by 
%   		Hintikka's Game-Theoretic-Semantics~\cite{GTS-Hintikka}.
%   \item Rather than participating in SGs directly, scholars participate in Contradiction-Agreement Games (CAGs). 
%   		CAG is a mechanism built on top of SGs and it can be used to meaningfully evaluate user strength and enable users 
%   		to meaningfully contribute to the crowd belief without the requirement that users must have contradictory 
%   		positions on the underlying claim.
%   \item It provides algorithms to estimate user strength and crowd beliefs based on the outcome of several CAGs.  
%   \item It uses \emph{labs} to define special interest groups of users. A lab is created by an owner (one kind of users) and 
%   		consists of a family of claims and a number of scholars (another kind of users) that are \emph{interested} in 
%   		studying these claims.
%   \item It relies on anonymity to discourage ``cheating''.
%   \item It leaves the exact lab interaction mechanism for lab owners to design.
% \end{enumerate}
% 

% \begin{enumerate}
%   \item the players agree on the claim, or a mechanism for choosing it,
%   \item the players chose opposing positions,
%   \item both players are properly incentivised (i.e. aiming at winning the game.). 
% \end{enumerate}
% 
% 
% Fair choice of claims.
% Arbitrary strength of scholars (open endedness).
% Proper incentivization (to some extent/ assume players want to score higher on strength measures).

\subsection{The Contradiction-Agreement Game}
\label{sec:CAG}
CAGs remove the restriction that scholars must take contradictory positions on claims. 
In case scholars take contradictory positions, CAG reduces to one SG. Otherwise, CAG 
reduces to two testing SGs. In a test SG, one of the scholars, the tester, is forced to take the opposite 
position of the position it chose. The two scholars switch their testing roles between 
the two games. Even though, the tester is forced to take a particular position, CAG-based evaluation remains fair. 
It also remains possible to get potentially correct contributions out of the testing games when the winner is 
not the forced tester. 

SGs with forced scholars can cause unfairness in two different ways:
\begin{enumerate}
  \item Winning against a forced scholar is not the same as winning against an unforced scholar. Giving both winners a point for winning 
  		would be unfair.
  \item The forced scholar is at a disadvantage.
\end{enumerate} 
To overcome these two problems, we adopt the rule that the scholar winning an SG \emph{scores} a point only if its adversary is not forced. 
Although, this solves the two problems, it, oddly enough, puts the winner at a disadvantage because it has no chance of \emph{scoring} a point.
Luckily, considering both test games together, the evaluation (i.e. payoff) is fair because both scholars have an equal chance of scoring. 
% \footnote{Note that $p1$ has no chance of winning the agreement T1 game and $p2$ has no chance of winning the agreement T2 game. 
% But taking the two games together, both players have an equal chance of winning.} 
% and that the payoff function never penalizes a forced player.
Furthermore, scholars remain properly incentivised to win under the payoff. This is important to ensure the fairness of user evaluation 
as well as the potential correctness of the contributions of the unforced winners. Our readers can verify these properties by inspecting 
Table~\ref{table:CAG} which summarizes CAGs. The columns of the table indicate the name of the SG being played, the forced scholar (if any), 
the SG winner, and whether the contribution of the winner is potentially correct (assuming that ``cheating'' is somehow discouraged).
% % The first two rows summarize the first test game where $p2$ is the tester.
% % The third and forth rows summarize the second game where $p1$ is the tester. 
% The first column indicate the SG being played. 
% The second column indicates the forced scholar. 
% The third column indicates the winner of the SG.
% The forth column indicates whether the contribution of the winner is potentially correct (assuming that 

% \begin{table}
% \centering
%     \begin{tabular}{|c|c|c|c|c|c|}
%         \hline
%         \# & $p_1$ forced & $p_2$ forced & winner & $payoff (p_1,p_2)$ & meaningful contribution \\ \hline
%         5  & f         & f         & $p_1$     & (1, 0)         & $p_1$                      \\ 
%         6  & f         & f         & $p_2$     & (0, 1)         & $p_2$                      \\ \hline
% %         7  & t         & t         & $p_1$     & (1, 0)         & --                      \\ 
% %         8  & t         & t         & $p_2$     & (0, 1)         & --                      \\
% %         \hline
%     \end{tabular}
% \caption{The Contradiction Game}
% \label{table:ContradictionGame}
% \end{table}
% 
% \begin{table}
% \centering
%     \begin{tabular}{|c|c|c|c|c|c|}
%         \hline
%         \# & $p_1$ forced & $p_2$ forced & winner & $payoff (p_1,p_2)$ & meaningful contribution \\ \hline
%         1  & f         & t         & $p_1$     & (0, 0)         & $p_1$                      \\ 
%         2  & f         & t         & $p_2$     & (0, 1)         & --                      \\ \hline
%         3  & t         & f         & $p_1$     & (1, 0)         & --                      \\ 
%         4  & t         & f         & $p_2$     & (0, 0)         & $p_2$                      \\
%         \hline
%     \end{tabular}
% \caption{The Agreement Game}
% \label{table:AgreementGame}
% \end{table}
% 
% 

\begin{table}
\centering
    \begin{tabular}{|c|c|c|c|c|c|}
        \hline
        \multirow{2}{*}{Game} & \multirow{2}{*}{forced} & \multirow{2}{*}{winner} & payoff & potentially correct \\
        &&&($p_1$, $p_2$) & contribution \\ \hline \hline 
        %Game & \# & forced & winner & payoff & meaningful contribution \\ \hline \hline
        \multirow{2}{*}{Agreement T1}
        & $p_2$         & $p_1$     & (0, 0)         & $p_1$                      \\ 
        & $p_2$         & $p_2$     & (0, 1)         & --                      \\ \hline 
        \multirow{2}{*}{Agreement T2}
        & $p_1$        & $p_1$     & (1, 0)         & --                      \\ 
        & $p_1$         & $p_2$     & (0, 0)         & $p_2$                      \\ \hline \hline
		\multirow{2}{*}{Contradiction} 
        & --         & $p_1$     & (1, 0)         & $p_1$                      \\ 
        & --         & $p_2$     & (0, 1)         & $p_2$                      \\
        \hline
    \end{tabular}
\caption{The Contradiction-Agreement Game}
\label{table:CAG}
\end{table}

% 
% Winning while not forced. 
% 
% forced win evidence  payoff
%   f     t    yes       1 win wile not forced
%   f     f    no        -1 lose
%   t     t    no        ? win while forced
%   t     f    no        0 lose 
%  
%  ===
%  winner  p1f   p2f  meaningful payoff(p1,p2)
%     p1    f     t     p1         (0, 0)
%     p2    f     t     --         (0, 1) ?? 2 wins while forced and 1 is not forced
%     p1    t     f     --         (1, 0) ?? 1 wins while forced and 2 is not forced
%     p2    t     f     p2         (0, 0)
% 
% ==
%  winner  p1f   p2f  meaningful payoff(p1,p2)
%     p1    f     t     p1         (0, 0)
%     p1    f     f     p1         (1, 0) SG
%     p1    t     t     --         (1, 0)
%     p1    t     f     --         (1, 0) ?? 1 wins while forced and 2 is not forced
%     p2    f     t     --         (0, 1) ?? 2 wins while forced and 1 is not forced
%     p2    f     f     p2         (0, 1) SG
%     p2    t     t     --         (0, 1)
%     p2    t     f     p2         (0, 0)
%     
%  forced players are incentivised to win. 
%     
%  winning against a forced player is still taken as evidence because the forced players are correctly incentivised to win.
%     
% 
\subsubsection{CAG Desirable Properties}
  CAG encourages innovation because forced scholars can score while their adversary cannot. This provides an incentive for 
  forced players to win SGs even though they are forced to take positions that are often contradictory to their own intuition 
  as well as to the crowd beliefs. 
  Also, CAGs ensure that some form of progress is taking place either as an update to the player scores or that a potentially 
  correct contribution has been made. Furthermore, in the first case, the loser is receiving targeted feedback and in 
  the second case, the community benefits from the potentially correct contribution.
%    
% \subsubsection{Progress Property}
% CAGs ensure that some form of progress is taking place either for individuals or for the community. This property can be stated
% as : ``there is either a win/loss or there is a meaningful contribution''. In the first case, the loser is receiving back targeted feedback 
% and in the second case, the community benefits from the meaningful contribution.

\newcommand{\payoff}[2]{P\!ayo\!f\!\!f\!\,(#1, #2)}  
\subsection{Evaluating User Strength}
\label{sec:userStrength}
We devised an algorithm to evaluate user strength based on CAG scores.
The algorithm weighs the scores by the strength of the adversary and calculates 
the strength of the scholar as the ratio of wins over the sum of wins and losses in order to even out 
the difference in the number of played CAGs \concern{2} as well as the difference in the strength of adversaries \concern{3}. 

Informally, the algorithm starts with an estimate of $1$ for the strength of all players. 
Then it computes the weighted wins and losses for each player based on the payoffs and the strength of their adversaries.
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.

Formally, we denote the sum of payoffs that scholar $S_1$ gets from scholar $S_2$ by $\payoff{S_1}{S_2}$. 
The strength of user $S$ is denoted by $Str(S)$. The algorithm is given by:

\begin{eqnarray*}
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)) \\
Total^{(k)}(S_i) &=& Wins^{(k)}(S_i) + Losses^{(k)}(S_i) \\
Str^{(k)}(S_i) &=& \begin{cases} Wins^{(k)}(S_i) / Total^{(k)}(S_i) , & \mbox{if } Total^{(k)} \neq 0 \\ 0.5, & \mbox{otherwise.} \end{cases}
\end{eqnarray*}
  
% This algorithm has the property that the impact of winning an extra point against a player with low (or high) strength will
% have a small (or large) negative impact on the strength of the losing player. This property is useful to even out the advantage 
% that one player might get over another player when players are not playing against the same set of adversaries. 

Ideally, we would like the strengths produced by the algorithm to be \emph{consistent} with the payoffs (i.e. 
$\forall S_1, S_2 : \payoff{S_1}{S_2} \geq \payoff{S_2}{S_1} \Rightarrow Str(S_1) \geq Str(S_2)$). 
However, the relation $R(S_1, S_2) = \payoff{S_1}{S_2} \geq \payoff{S_2}{S_1}$ is not necessarily transitive while 
the relation $Q(S_1, S_2) = Str(S_1) \geq Str(S_2)$ is. However, we conjecture that the strengths produced by our algorithm 
minimize such inconsistencies.

However, the the algorithm possesses the following weaker soundness properties:
\begin{enumerate}
%  \item The evaluated strength is \emph{consistent} with the payoff. Formally, $\forall p_1, p_2 : Payoff(p_1, p_2) \geq Payoff(p_2, p_1) \Rightarrow Str(p_1) \geq Str(p2)$.
  \item A scholar $S_i$ that beats the score of another scholar $S_j$ on their mutual games as well as on games with all other scholars $S_k$ will have a higher strength.  
  $\forall i, j \payoff{S_i}{S_j} > \payoff{S_j}{S_i} \wedge \forall k \neq i, j : \payoff{S_i}{S_k} \geq \payoff{S_J}{S_k} \wedge \payoff{S_j}{S_k} \leq \payoff{S_i}{S_k} \Rightarrow Str(S_i) \geq Str(S_j)$.
  \item A scholar that only won(lost) games will have a strength of $1$($0$). Formally, 
  		$\forall i \forall j \payoff{S_i}{S_j} = 0 \wedge \exists j \payoff{S_j}{S_i} > 0 \Rightarrow Str(S_i) = 0$, and 
  		$\forall i \forall j \payoff{S_j}{S_i} = 0 \wedge \exists j \payoff{S_i}{S_j} > 0 \Rightarrow Str(S_i) = 1$. 
  		A scholar that has not won or lost any games will have a strength of $0.5$. Formally, 
  		$\forall i \forall j \payoff{S_j}{S_i} = 0 \wedge \payoff{S_i}{S_j} = 0 \Rightarrow Str(S_i) = 0.5$.
  %Once a player looses a single point, its strength becomes dependent on the strength of other player.
  % \item The final strength of the players is \emph{independent} of the order in which points are acquired.
\end{enumerate}


% 
% The soundness of the algorithm is based on the following two properties: 
% 
% %   \item Loosing a point against a player with low strength will produce a large negative impact, while loosing a point against a scholar with a high strength will have a small negative impact.
% %   \item (The dual) Winning a point against a player with high strength will produce a large positive impact, while winning a point against a player with low strength will have a small positive impact.
% 
% The proposed algorithm has the following attractive properties:
% \begin{enumerate}
% %  \item The evaluated strength is \emph{consistent} with the payoff. Formally, $\forall p_1, p_2 : Payoff(p_1, p_2) \geq Payoff(p_2, p_1) \Rightarrow Str(p_1) \geq Str(p2)$.
%   \item A player that only won(lost) games will have a strength of $1$($0$). Formally, $\forall j \payoff{S_i}{S_j} = 0 \wedge(S_)$
%   \item $\forall i,j,k : \payoff{S_i}{S_k} \geq \payoff{S_J}{S_k} \wedge \payoff{S_j}{S_k} \leq \payoff{S_i}{S_k} \Rightarrow Str(S_i) \geq Str(S_j)$.
%   %Once a player looses a single point, its strength becomes dependent on the strength of other player.
%   % \item The final strength of the players is \emph{independent} of the order in which points are acquired.
% \end{enumerate}
% 
% The first three properties are related to soundness. 
% The third property is related to the absence of learning between individual games. This property can be invalid if the games are played  
% across a period of time that is large enough to allow learning.
% The last two properties are important to make the evaluation fair even though a player might have played against only strong/weak players.

\subsection{Evaluating Crowd Beliefs}
\label{sec:crowdbeliefs}
 We consider the positions taken by non-forced CAG winners to be providing the community with an evidence that these 
 positions are correct. We take the strength of the losing user as the weight of such evidence. 
 For each claim $c$ we let $c_T$ be the sum of the weights of all evidences that $c$ is true, $c_F$ be the sum of the 
 weights of all evidences that $c$ is false. The believed likelihood that $c$ is true is $C_T/(C_T + C_F)$. 
 Similarly, the believed likelihood that $c$ is false is $C_F/(C_T + C_F)$.

% To move later:
% ==============
% \subsection{Lab Interaction Mechanisms}
%  Lab owners are responsible for developing a mechanism to match players and to select claim. The mechanism is expected to 
%  fairly select claims and to ensure that CAGs are interesting. 
%  Below we provide three examples of fair claim selection mechanisms:
% 
%  \begin{enumerate}
%    \item \emph{CAG matches}: which have an even number of rounds. In each round, one player chooses the claim. Players alternate 
%    						the role of choosing claims. A generalization is to play a cut-and-choose game ~\cite{sep-logic-games} where
%    						in each round, one players chooses a set of claims (a cut) then the adversary chooses a claim from the set.
%    						
%    \item \emph{Trusted owner}: the lab includes an algorithm for selecting claims. For example, suppose that 
%    the purpose of the lab is 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 CAG.
%      
%    \item \emph{Battleship mechanism}: users independently propose claims to the system. When two scholars propose the same
% 		claim, the system collects their position and then engages them in a CAG.
%  \end{enumerate}
%   
%   For player matching mechanisms, the lab can use one of the existing schemes such as round-robin or swiss-style tournaments. 
%   Alternatively, the lab can match players based on their preferences.
% 
%   Labs can also include other game mechanics such as leader boards and badges for a number of qualities such as strength, 
%   learning(improvement in strength), participation (number of games played) and breakthroughs. 
%    


% \subsection{Experience with the SCG}
% \label{ExperienceSection}
% We report on our experience with the Scientific Community Game (SCG), 
% a predecessor of our current system. SCG has evolved since 2007. 
% We have used the SCG in software development courses at both the undergraduate
% and graduate level and in several algorithms courses~\cite{KarlTeaching}.
%    
% \subsubsection{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.
% 
% \subsubsection{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 JSON
% which allowed the students to use a wide variety
% of programming languages to implement their algorithms.
% 
% The students collaboratively solved several problems
% such as the problem
% of finding the worst-case inputs for the Gale-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{Experience with the SCG}
\label{ExperienceSection}
The SCG has evolved since 2007. We have used the SCG in
software development courses at both the undergraduate
and graduate level and in several algorithm courses.
Detailed information about those courses is available from
the second author's teaching page.

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

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

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

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

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

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

\subsection{Crowdsourcing and Human Computation}

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

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

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

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

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


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

\subsection{Foundations of Digital Games}

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

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

\subsection{Architecting Socio-Technical Ecosystems}

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

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

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

\subsection{Online Judges}

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

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

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

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

\subsection{Scientific Method in CS}

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

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

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


\subsection{Origins of SCG}

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


\section{Conclusion and Future work}
We presented SCG, a crowdsourcing platform for computational problems.
SCG provides a simple interface to a community that uses the (Popperian) Scientific Method.
Our future work includes further development to the current system, its underlying model, as well as to evaluate our system. 

\subsection{Model Development}
\subsubsection{Claim Family Relations and Meta Labs}
Relations computational problems can be used to \emph{test} implementations of their solution algorithms. Reduction is an important 
kind of relation between computational problems that can be used to \emph{prove} certain impossibility results 
as well as to enable the implementation of one computational problem to \emph{reuse} the implementation of another computational problem.

In our system, these relations can be expressed as claims between claim families specifying computational problems.  
% It is worth mentioning that 
% relations between claim families can be either purely logical or be grounded in the relationship between their underlying models. 
For example, consider the following two claim families:
\begin{enumerate}
 \item \emph{Size of minimum graph basis}: a basis of a directed graph $G$ is defined as set of nodes such that 
  any node in the graph is reachable from some node in the basis. Formally,    
  $MinBasisSize(G \in Digraphs, n \in \mathbb{N}) = BasisSize(G, n) \wedge \forall k~s.t.~k < n : \neg BasisSize(G, k)$ where
  $BasisSize(G \in Digraphs, n \in \mathbb{N}) = \exists s \in \mathcal{P}(nodes(G))~s.t.~|s|=n~:\forall m \in nodes(G)~\exists p \in paths(G): first(p) = m \wedge last(p) \in s$.
 \item \emph{Number of source nodes of a DAG}: a source node is a node with no incoming edges. Formally, 
  $\#src(D \in DAGs, m \in \mathbb{N}) = \exists s \in \mathcal{P}(nodes(D))~s.t.~|s|=m~:\forall v \in nodes(D) : inDegree(v) = 0 \Leftrightarrow v \in s$.
\end{enumerate}
The relation between the two claim families $MinBasisSize(G \in Digraphs, n \in \mathbb{N})$ and $\#src(D \in DAGs, m \in \mathbb{N})$ 
can be described by 
$\forall G \in Digraphs, n \in \mathbb{N}~: MinBasisSize(G, n) = \#src(SCCG(G), n)$ where $SCCG$ refers to Tarjan's the Strongly Connected Component Graph algorithm.

Like other claims, claims about relations between claim families can be studied in a regular lab in our system. 
However, we see a potential to further utilize these claims to cross check crowd beliefs across labs and to translate user contributions  
across labs. 
% In the context of our system, relations between claim families are also useful as a tool for checking the set of user contributions 
% making up the crowd beliefs.
% In the case when the relation between claim families can be expressed as a \emph{truth preserving function}, 
% %Order preserving functions (i.e. monotonic) , functions preserving a particular property
% it is possible to translate some of the contributions from one lab to the other labs. To study the relationship between claim families 
% of other labs and at the same time further utilize these relationships, 
% 
To harness this potential, we propose to add meta labs to our system. More specifically, we propose to answer 
the two following questions:
\begin{enumerate}
  \item How can our system further utilize relations between claim families beyond regular claims?
  \item How to express meta labs so that it is possible to further utilize them in an automated way?
\end{enumerate}

\subsubsection{Generalized Claims}
Users can lose SGs involving optimization problems even if their solutions can be \emph{almost} optimal. For example, consider the 
following claim: 
$\forall p \in Problem: \exists s \in Solution :\forall t \in Solution : better(quality(s, p),quality(t, p))$
It is enough for the opponent to provide a \emph{slightly} better solution to win.
As remedy, it is possible to bias the situation towards the proponent by requiring the opponent to provide 
at solution that is at well better than the solution provided by the proponent in order to win. The following claim 
illustrates this solution: 
$\forall p \in Problem :\exists s \in Solution :\forall t \in Solution : within10\%(quality(s, p),quality(t, p))$
It is also possible to generalize the claims such that the larger the quality gap is the more of a payoff the winner gets. 
For example, assuming the $distance$ function returns a number between $-1$ and $1$, the following generalized claim illustrates this solution:
$\forall p \in Problem :\exists s \in Solution :\forall t \in Solution : distance(quality(s, p),quality(t, p))$
We propose to develop a systematic approach for computing the payoff in SGs for generalized claims.

\subsection{System Development}
 We propose to turn the current implementation ~\cite{CurrentImpl} into a web based application. We also propose to further 
 develop the claim language and the CIM and the encouragement and retention scheme.%, and visualizations of the crowd beliefs.
\subsubsection{Claim Language}
 There are certain game related concerns that cannot be expressed in the current claim language. Furthermore, the current 
 language is not as user friendly as it could be. To overcome these two problems, we propose to make the following enhancements to 
 the claim language:
 \begin{enumerate}
   \item make the claim language support second order logical sentences. This enables the claim language to express properties about
   		the resource consumption of algorithms. For example, 
   		$AlgoRunTime(c, n_{min}, n_{max}) = \exists a \in Algo : \forall i \in Input~s.t.~ n_{min} \leq size(i) \leq n_{max}: correct(i, a(i)) \wedge RunTime(a(i)) <= c * size(i) $.\\
   		Second order logical sentences can also express the dependence (or independence) of atoms through Skolem functions. Other approaches to express the 
   		dependence concerns is through either the dependence friendly logic or the independence friendly logic~\cite{dependenceLogic}. 
   \item add a $let$ binder for efficiency. For example, to avoid computing $a(i)$ twice in $AlgoRuntime$.
   \item add syntactic forms, in addition to $Formula$, to provide a more user friendly support of different kinds of computational problems (such as search, optimization, counting problems). 
   		For example, to enable users to write: $sat(f) =  \max_{J} csat(f,J)$, instead of: $sat(f, x) = \exists J~s.t.~csat(f, J) = x : \forall H : csat(f, H) \leq csat(f, J)$
   \item add an abstraction facility. %fabstraction facilities / support new constructs
 \end{enumerate}
 
\subsubsection{Crowd Interaction Mechanism}
We propose to implement the following CIM. 
Lab owners establish Swiss-style CAG tournaments between scholars in the lab in order to drive interactions in the lab. 
Swiss-style tournaments have the property of matching players with similar strength and therefore enhancing the users' 
experience \concern{10} as well as fairness \concern{3}. Claims can be chosen by one of the following approaches:
\begin{enumerate}
	   \item \emph{CAG matches}: CAG matches consist of an even number of CAGs. Each scholar chooses the claim for exactly 
	   							half of the CAGs. Claims must be chosen from 
	   							the lab's claim family. A generalization of this approach is to play a cut-and-choose game 
	   							~\cite{sep-logic-games} where in each round, one players chooses a set of claims 
	   							(a cut) then the adversary chooses a claim from the set.
	
	   \item \emph{Owner dictated}: 
	   the lab owner provides an algorithm for selecting claims to achieve a particular purpose. For example, if the purpose 
	   is to clean the contribution database, then the algorithm would select claims underlying scholar contributions 
	   in the contribution database. The purpose could also to solve a particular subset of open problems or to solve a 
	   computational problem in a particular approach, delegating subproblems to the 
	   crowd. For example, the purpose could be to \emph{plot} the relationship between 
	   a particular claim family parameter and the correctness of the claim. 
% 			   
% 			   the lab includes an algorithm for selecting claims. For example, suppose that
% 			   the purpose of the lab is 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.
% 			
	   \item \emph{Battleship style}: use a claim that both scholars had previously contributed a position on.
% 			   the same claim to the contribution database.
\end{enumerate}

A distinctive feature of this CIM is that scholars never choose their adversaries. 
This is important to discourage ``cheating'' \concern{4,6}. A second feature is that CIM \emph{memoizes} winning positions taken 
by scholars and never asks scholars to provide these positions in subsequent CAGs until scholars fail to defend these positions. 
The contribution database plays the role of the cache for winning positions. This is important to discourage ``cheating'' \concern{6}. 
It is also important that the CIM allows scholars to revise their previously established contributions to avoid losing future CAGs    

\subsubsection{Encouragement and Retention Scheme}
We suppose that scholars will aspire to have the highest scores on meaningful performance measures. The system can establish the 
scores for players and provide few different views, such as a leaderboard, for scholars to encourage score based competition.
In addition to strength, we propose to develop the following complementary measures:
\begin{enumerate}
  \item \emph{Breakthrough contribution} : When required to do so, scholars might provide well known claims that they know how to defend. 
  The purpose of developing a measure for breakthrough contributions is to encourage scholars to propose new claims and take positions 
  opposing to the crowd beliefs.
  \item \emph{Learning} : Learning is an indirect contribution of scholars. We propose to assess learning through the change in scholar's 
  strength as well as through scholar's revisions to its own established contributions.  
  \item \emph{Crowd preference} : Scholars might be able to spot certain attractive properties of a particular contribution. 
  The idea is to enable scholars to ``like'' contributions and essentially count the ``likes'' the contributions of a particular scholar gets.
\end{enumerate}

Another potential encouragement and retention scheme that we want to explore is to have an underlying theme where scholars are 
represented by customizable virtual avatars. This enhances the engagement as scholars can become invested in customizing 
their avatars besides it makes it easier for scholars to be embodied in CAGs by their avatar. 


   
\subsection{Evaluation}
We propose to conduct a two part evaluation of effectiveness of our system in leveraging the problem solving ability of the crowd. 
The first part consists of evaluating the quality of the algorithms produced by the crowd to solve non-trivial computational problems. 
We propose to compare those algorithms to the best known algorithms. Examples include the max cut problem and the highest safe rung problems.
The second part consists of comparing the quality of the algorithms produced by the crowd through our system to algorithms produced 
through traditional crowdsourcing competitions. Examples include the genome-sequencing-problem~\cite{harvard-genome-sequencing}.

We propose to also use our crowdsourcing system to evaluate a number of its components and their properties. 



\bibliographystyle{theapa}	
\bibliography{references}
\begin{appendices}


\section{Claim Language}
\label{section:ClaimLang}
A claim is an interpreted statement in first order predicate logic. A claim consists of an underlying model $M$, 
a predicate formula $\phi$ potentially containing free variables, an assignment $g$ for the free variables in $\phi$.

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 ")".
Negated = "(" "not" <formula> Formula ")".
Connective = And | Or.
And = "and".
Or = "or".

Quantified = <quantification> Quantification <formula> Formula.
Quantification = "(" <quantifier> Quantifier 
               <var> ident 
               "in" <type> ident
               <qPred> 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}

\section{Semantic Games}
\label{section:SGDef}
Given a claim \code{c} and two scholars, a proponent $ver$ and a opponent $fal$. Let $M$ be the underlying model of \code{c}, 
let $\phi$ be the formula and $g$ be \code{c}'s assignment to the free variables in $\phi$.
We define the semantic game of $ver$ and $fal$ centered around \code{c} \code{SG(c,}$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{proponent} and \code{opponent}, the \code{winner}, the assignment \code{g}, 
% and a \code{timestamp}.

\end{appendices}

\end{document}