\documentclass [12pt] {article}
\usepackage {epsfig, latexsym}

\begin{document}
\parskip= 2pt
%\date{}

\newcommand {\ignore} [1] {}

\def \bfm {\bf \boldmath}

\def \AA {{\cal A}}
\def \BB {{\cal B}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{myrule}{Rule}[section]
\newenvironment{proof}{\noindent{\bf Proof:\/}}{\hfill $\Box$\vskip 0.1in}

  %Marginal notes for communicating with coauthors
\setlength{\marginparwidth}{1.2in}
\setlength{\marginparpush}{-5ex}
\newif\ifnotesw\noteswtrue% T to show box & marginal notes; F suppresses.
\newenvironment{change}%
   {\ifnotesw\marginpar[\hfill\(\top\)]{\(\top\)}\fi}%
   {\ifnotesw\marginpar[\hfill\(\bot\)]{\(\bot\)}\fi}
\newcommand{\deletion}{\ifnotesw\marginpar[\hfill\(\vartheta\)]{\
(\vartheta\)}\fi}
\newcommand{\mnote}[1]%
    {\ifnotesw\marginpar%
        [{\scriptsize\it\begin{minipage}[t]{\marginparwidth}\raggedleft#1%
                        \end{minipage}}]%
        {\scriptsize\it\begin{minipage}[t]{\marginparwidth}\raggedright#1%
                        \end{minipage}}%
    \fi}

\newcommand {\mnr} [1] {\mnote {rf: #1} } % Referree note
\newcommand {\mny} [1] {\mnote {YD: #1} } % Lecturer note
\newcommand {\mna} [1] {\mnote {au: #1} } % Author note

\title{Negation Transformation}

\author{
Yefim Dinitz \thanks{
		Department of Computer Science, 
		Ben-Gurion University of the Negev, 
		POB 653, Beer-Sheva 84105 Israel.
		{\tt E-mail: dinitz@cs.bgu.ac.il}.}
	     \and
Avraham Israeli \thanks{...}
	}

\maketitle


\section{Introduction}

\subsection{Motivation}

   We would like to achieve two aims, in this paper.
The first one is to recall important rules, used often in proofs, and
the second one is to excersise in LaTeX \cite{Lam}.

\subsection{Our Problem}

   Assume, we like to proof a statement, defined by
a complex logical formula (LF, for short).
Our way of proof is by contradiction (``hohacha be-shlila'').
It is very important to formulate well the opposite statement,
in order to not err when bringing it to a contradiction.
The desired property is {\it absence of negation before any
complex logical subformula}.

   Luckily, there are a few logical rules, related to negation
applied to a quantifier, or to a locical operation, such as ``AND'', etc.
Using those rules, we are able to transform the negation of any LF
to the form, where negation is applied to elementary, in a sense,
subformulae only.

   There are many textbooks, containing a similar result,
see e.g., \cite{TB1,TB2}.

   The structure of the paper is as follows.
Section~\ref{s:def-r} presents our definitions, and known rules.
In Section~\ref{s:main}, we formulate our main result,
and suggest a proof, for it.

   
\section{Definitions and Known Rules}
\label{s:def-r}

   Let us assume, for simplicity, that operations ``AND'' and ``OR''
have exactly two operands, in a logical formula.

\begin {definition}
\label{d:el}
   We say that an LF is elementary, if it is not neither
negation of another LF, nor a quantifier expression,
nor an ``AND'' or ``OR'' expression.
\mny {See comment~\ref{c:YD1} at the end.}
\end {definition} 

  . . .

\begin {definition}
   . . .
\end {definition}

   . . .

\begin {myrule} [For All]
\label{r:all}
   $\neg \forall \langle arg \rangle: \langle LF \rangle
\Longleftrightarrow
   \exists \langle arg \rangle: \neg \langle LF \rangle \ .$
\end {myrule}

\begin {myrule} [And]
\label{r:and}
   $\neg ( \langle LF1 \rangle  \wedge \langle LF2 \rangle )
\Longleftrightarrow
   \neg \langle LF1 \rangle \vee \neg \langle LF2 \rangle \ .$
\end {myrule}


\section{Main Statement}     \label{s:main}

   . . . 

\begin {theorem} 
   . . .
\end {theorem}

\begin {proof}
   It is obvious, using Rules~\ref{r:all} and \ref{r:and}.
\mnr {much too short}
Moreover, no my friend that I asked him on, met an objection
to this statement. \mny {Ma ze} \mny {???}
\end {proof}


\begin{thebibliography} {99}

\bibitem{Lam}
L.~Lamport. A Document Preparation System LaTeX.
Addison-Wesley, 1994.

	\ignore {
\bibitem{DF}
M. Dyer and A. Frieze.
Probabilistic analysis of the multi-dimensional knapsack problem.
{\it Math. of OR} 14, 162-176 (1989).
}

\end{thebibliography}

\section {Comments}

\begin {enumerate}
\item 
   {\bf Attention:} 
   Not to forget to run a spell checker
(e.g., ispell $<$file name$>$, in unix).
\item \label{c:YD1}
   This is to show how to make enumerated itemization, and
how to organize not a-couple-of-words comments.
\end {enumerate}

\end {document}