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

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


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

% from bionetics
\newcommand\demj{DemeterJ}

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

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

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


\input{definitions2}
% 
% \section{Protocol}
% 
% \section{Proofs}
% 
% let $RefutationGame(P1, P2, C)$ be the extensive form representation
% of the game between a the two players $P1$ and $P2$ for refuting the claim $C$ 
% using the protocol $C.lab.Proto$, and the refutation predicate $C.lab.Pred$.
% 
% Faulty actions:
%  $Alice$ proposes $C$ and $P2$ has a winning strategy in $RefutationGame(P1, P2, C)$.
% Exposing action:
%  $Bob$ decides to refute $C$.
% Justification:
%   According to the SCG binary game rules. In this case, the SCG reduces to playing
%  $RefutationGame(Alice, Bob, C)$ for which there is a winning strategy for $Bob$.
%  
% Faulty actions:
%  $Bob$ refutes a claim $C$ proposed by $Alice$ where $P1$ has a wining strategy 
%  in $RefutationGame(P1, P2, C)$.
% Exposing action:
%  None.
% Justification:
%   According to the SCG binary game rules. In this case, the SCG reduces to playing
%  $RefutationGame(Alice, Bob, C)$ for which there is a winning strategy for $Alice$.
% 
% Faulty actions:
%  $Bob$ aggrees with a claim $C$ proposed by $Alice$ where $P2$ has a winning strategy 
%  in $RefutationGame(P1, P2, C)$.
% Exposing action:
%  None.
% Justification:
%   According to the SCG binary game rules. In this case, the SCG reduces to playing
%  $RefutationGame(Alice, Bob, C)$ for which there is a winning strategy for $Alice$.
%  
% A claim $C$ is said to be optimum if it is the strongest claim such that there is 
% a winning strategy for $P1$ in $RefutationGame(P1, P2, C)$.
% 
% Faulty actions:
%   $Alice$ proposes a claim $C$ where $C$ is not optimum.
% Exposing action:
%   $Bob$ strengthens $C$ to $C'$ such that there is a wining strategy for $Bob$ in 
%   $RefutationGame(Bob, P2, C')$.
% Justification:
%   According to the SCG binary game rules. In this case, the SCG reduces to playing
%   $Refutation(Bob, Alice, C')$ for which $Bob$ has a wining strategy. 
% 
% Faulty actions:
%   $Bob$ strengthens a claim $C$ proposed by $Alice$ to $C'$ where $C$ is optimum.
% Exposing action:
%   None.
% Justification:
%   According to the SCG binary game rules, $C'$ must be stronger than $C$, but by definition
%   $C$ is the strongest claim such that there is a wining strategy for $Bob$ in 
%   $RefutationGame(Bob, P2, C)$. Therefore, there is no wining strategy for $Bob$.
%   
% Faulty actions:
%   $Bob$ aggrees with a claim $C$ proposed by $Alice$ where $C$ is not optimum.
% Exposing action:
%   None.
% Justification:
%   None.
% 
%   

\end{document}
