%%%%%%%%%%%%%%%%%%%%%%%%% The Journal of Logic Programming
%%%%%%%%%%%%%%%%%%%%%%%%% Elsevier Science Publishing Company, Inc.
%%%%%%%%%%%%%%%%%%%%%%%%% 655 avenue of the Americas
%%%%%%%%%%%%%%%%%%%%%%%%% New York, N.Y. 10010
%%%%%%%%%%%%%%%%%%%%%%%%% U.S.A.
%%%%%%%%%%%%%%%%%%%%%%%%% Ver. 1.0 Sept. 24, 1993
\typeout{JLP Version 1.0 <Sept. 24, 1993>}
\def\bull{$\Box$}
\def\ell{l}
%\def\halmos{\rule{6pt}{6pt}}
\def\halmos{$\Box$}
\def\em{\protect\pem{}}
\def\pem{\ifdim \fontdimen\@ne\font >\z@ \rm \else \it \fi}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% If you do not wish to use the below environments comment them out.
%%%%%%% Only the block of code labeled with %**** are the lines you should
%%%%%%% place a % in front of.  The numbering will be by section.
\newcounter{theorem}[section]                                            %****
\newcounter{algorithm}[section]                                          %****
\newcounter{corollary}[section]                                          %****
\newcounter{proposition}[section]                                        %****
\newcounter{lemma}[section]                                              %****
\newcounter{axiom}[section]                                              %****
\newcounter{definition}[section]                                         %****
\newcounter{remark}[section]                                             %****
\newcounter{comment}[section]                                            %****
\newcounter{example}[section]                                            %****
\newcounter{problem}[section]                                            %****
\newcounter{conjecture}[section]                                         %****
\newcounter{observation}[section]                                        %****
\newcounter{acknowledgements}[section]                                   %****

\newtheorem{theorem}{Theorem}[section]                                   %****
\newtheorem{axiom}{Axiom}[section]                                       %****
\newtheorem{lemma}{Lemma}[section]                                       %****
\newtheorem{corollary}{Corollary}[section]                               %****
\newtheorem{proposition}{Proposition}[section]                           %****
\newtheorem{algorithm}{Algorithm}[section]                               %****
\newtheorem{observation}{Observation}[section]                           %****

\long\gdef\numberbysection{\renewcommand{\thesection}{\arabic{section}}
\renewcommand{\theequation}{\thesection.\arabic{equation}}
\@addtoreset{equation}{section}
\renewcommand{\thetheorem}{\thesection.\arabic{theorem}}
\@addtoreset{theorem}{section}
\renewcommand{\thefigure}{foo\thesection.\arabic{figure}}
\@addtoreset{figure}{section}
\renewcommand{\thetable}{\thesection.\arabic{table}}
\@addtoreset{table}{section}
\renewcommand{\thelemma}{\thesection.\arabic{lemma}}
\@addtoreset{lemma}{section}
\renewcommand{\theobservation}{\thesection.\arabic{observation}}
\@addtoreset{observation}{section}
\renewcommand{\thealgorithm}{\thesection.\arabic{algorithm}}
\@addtoreset{algorithm}{section}
\renewcommand{\thecorollary}{\thesection.\arabic{corollary}}
\@addtoreset{corollary}{section}
\renewcommand{\theproposition}{\thesection.\arabic{proposition}}
\@addtoreset{proposition}{section}
\renewcommand{\theaxiom}{\thesection.\arabic{axiom}}
\@addtoreset{axiom}{section}
\renewcommand{\theproblem}{\thesection.\arabic{problem}}
\@addtoreset{problem}{section}
\renewcommand{\theexample}{\thesection.\arabic{example}}
\@addtoreset{example}{section}
\renewcommand{\theremark}{\thesection.\arabic{remark}}
\@addtoreset{remark}{section}
\renewcommand{\thedefinition}{\thesection.\arabic{definition}}
\@addtoreset{definition}{section}
\renewcommand{\theconjecture}{\thesection.\arabic{conjecture}}
\@addtoreset{conjecture}{section}
\renewcommand{\thecomment}{\thesection.\arabic{comment}}
\@addtoreset{comment}{section}}

%%% Removed by SMS  Fri Apr 22 08:34:03 1994	
%%% because it DOESN'T MAKE ANY SENSE!
%%% The \thefigure gets re-redefined anyway later on, so what's the
%%% point of doing it here and letting it get clobbered!
%\numberbysection                                                         %****

\newenvironment{definition}[1]{\bgroup\vspace{12pt}                      %****
\hangindent=1pc\hangafter=1\noindent\it Definition\it\                   %****
\refstepcounter{definition}\thesection.\thedefinition.\quad\rm           %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

\newenvironment{remark}[1]{\bgroup\vspace{12pt}                          %****
\hangindent=1pc\hangafter=1\noindent\it Remark\it\                       %****
\refstepcounter{remark}\thesection.\theremark.\quad\rm                   %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

\newenvironment{comment}[1]{\bgroup\vspace{12pt}                         %****
\hangindent=1pc\hangafter=1\noindent\it Comment\it\                      %****
\refstepcounter{comment}\thesection.\thecomment.\quad\rm                 %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

\newenvironment{example}[1]{\bgroup\vspace{12pt}                         %****
\hangindent=1pc\hangafter=1\noindent\it Example\it\                      %****
\refstepcounter{example}\thesection.\theexample.\quad\rm                 %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

\newenvironment{problem}[1]{\bgroup\vspace{12pt}                         %****
\hangindent=1pc\hangafter=1\noindent\it Problem\it\                      %****
\refstepcounter{problem}\thesection.\theproblem.\quad\rm                 %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

\newenvironment{conjecture}[1]{\bgroup\vspace{12pt}                      %****
\hangindent=1pc\hangafter=1\noindent\it Conjecture\it\                   %****
\refstepcounter{conjecture}\thesection.\theconjecture.\quad\rm           %****
#1}{\par\vspace{1pt}\indent\egroup}                                      %****

%%%%%%% Do not comment out or uncomment anything
%%%%%%% below this line.  There are no more labeled lines.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\@normalsize{\@setsize\normalsize{12pt}\xpt\@xpt
\abovedisplayskip 12pt plus12pt minus5pt%
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip  \z@ plus12pt%
\belowdisplayshortskip  6pt plus12pt minus4pt}

\def\small{\@setsize\small{11pt}\ixpt\@ixpt
\abovedisplayskip 11pt plus 11pt minus 5pt%
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus6pt%
\belowdisplayshortskip 6pt plus6pt minus 4pt
\def\@listi{\topsep 4pt plus 2pt minus 2pt\parsep 2pt plus 1pt minus 1pt
\itemsep \parsep}}

\def\footnotesize{\@setsize\footnotesize{10pt}\viiipt\@viiipt
\abovedisplayskip 10pt plus 10pt minus 5pt%
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus 5pt%
\belowdisplayshortskip 5pt plus 5pt minus 3pt
\def\@listi{\topsep 3pt plus 1pt minus 1pt\parsep 2pt plus 1pt minus 1pt
\itemsep \parsep}}

\def\scriptsize{\@setsize\scriptsize{8pt}\viipt\@viipt}
\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
\def\large{\@setsize\large{14pt}\xiipt\@xiipt}
\def\Large{\@setsize\Large{18pt}\xivpt\@xivpt}
\def\LARGE{\@setsize\LARGE{22pt}\xviipt\@xviipt}
\def\huge{\@setsize\huge{25pt}\xxpt\@xxpt}
\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt}

\normalsize  % Choose the normalsize font.

%  ****************************************
%  *            PAGE LAYOUT               *
%  ****************************************

% All margin dimensions measured from a point one inch from top and side
% of page.

\newdimen\fullwidth
\newdimen\leftmarginwidth
\newdimen\emptyfoot
\newdimen\emptyhead
\newdimen\templength@
\fullwidth=33pc
\leftmarginwidth=3pc
\def\longhrule{\par\hbox to30pc{\kern-3pc
               \hrulefill}\par}

% SIDE MARGINS:
\if@twoside                % Values for two-sided printing:
   \oddsidemargin  3pc     % Left margin on odd-numbered pages.
   \evensidemargin 3pc     % Left margin on even-numbered pages.
   \marginparwidth 3pc     % Width of marginal notes.
\else                      % Values for one-sided printing:
   \oddsidemargin  3pc     % Note that \oddsidemargin = \evensidemargin
   \evensidemargin 3pc
   \marginparwidth 3pc
\fi
\marginparsep 11pt         % Horizontal space between outer margin and
                           % marginal note

% VERTICAL SPACING:
                         % Top of page:
\topmargin 27pt          % Nominal distance from top of page to top of
                         % Box containing running head.
\headheight 13.4pt       % Height of box containing running head.
\headsep 24pt            % Space between running head and text.
\topskip = 10pt          % '\baselineskip' for first line of page.
                         % Bottom of page:
\footskip 18pt           % Distance from baseline of box containing foot
                         % To baseline of last line of text.

% DIMENSION OF TEXT:
% 24 Jun 86: changed to explicitly compute \textheight to avoid roundoff.
% The value of the multiplier was calculated as the floor of the
% old \textheight minus \topskip, divided by \baselineskip for \normalsize.
% The old value of \textheight was 528pt.
% \textheight is the height of text (including footnotes and figures,
% excluding running head and foot).

\textheight = 48\baselineskip
\advance\textheight by \topskip
\textwidth 30pc                  % Width of text line.
                                 % For two-column mode:
\columnsep 10pt                  % Space between columns
\columnseprule 0pt               % Width of rule between columns.

% A \raggedbottom command causes 'ragged bottom' pages: pages set to
% natural height instead of being stretched to exactly \textheight.

% FOOTNOTES:

\footnotesep 6.65pt   % Height of strut placed at the beginning of every
                      % footnote = height of normal \footnotesize strut,
                      % so no extra space between footnotes.

\skip\footins 16pt plus 4pt minus 0pt % Space between last line of text and
                                      % top of first footnote.

% FLOATS: (a float is something like a figure or table)

%  FOR FLOATS ON A TEXT PAGE:

%ONE-COLUMN MODE OR SINGLE-COLUMN FLOATS IN TWO-COLUMN MODE:
\floatsep 12pt plus 2pt minus 2pt      % Space between adjacent floats moved
                                       % to top or bottom of text page.
\textfloatsep 20pt plus 2pt minus 4pt  % Space between main text and floats
                                       % at top or bottom of page.
\intextsep 12pt plus 2pt minus 2pt     % Space between in-text figures and
                                       % text.
\@maxsep 20pt                          % The maximum of \floatsep,
                                       % \textfloatsep and \intextsep (minus
                                       % the stretch and shrink).
%TWO-COLUMN FLOATS IN TWO-COLUMN MODE:
\dblfloatsep 12pt plus 2pt minus 2pt     % Same as \floatsep for double-column
                                         % figures in two-column mode.
\dbltextfloatsep 20pt plus 2pt minus 4pt % \textfloatsep for double-column
                                         % floats.
\@dblmaxsep 20pt                         % The maximum of \dblfloatsep and
                                         % \dbltexfloatsep.

%  FOR FLOATS ON A SEPARATE FLOAT PAGE OR COLUMN:
%    ONE-COLUMN MODE OR SINGLE-COLUMN FLOATS IN TWO-COLUMN MODE:
\@fptop 0pt plus 1fil    % Stretch at top of float page/column. (Must be
                         % 0pt plus ...)
\@fpsep 8pt plus 2fil    % Space between floats on float page/column.
\@fpbot 0pt plus 1fil    % Stretch at bottom of float page/column. (Must be
                         % 0pt plus ... )

%   DOUBLE-COLUMN FLOATS IN TWO-COLUMN MODE.
\@dblfptop 0pt plus 1fil % Stretch at top of float page. (Must be 0pt plus
                         % ...)
\@dblfpsep 8pt plus 2fil % Space between floats on float page.
\@dblfpbot 0pt plus 1fil % Stretch at bottom of float page. (Must be
                         % 0pt plus ... )
% MARGINAL NOTES:

\marginparpush 5pt       % Minimum vertical separation between two marginal
                         % notes.

%  ****************************************
%  *           PARAGRAPHING               *
%  ****************************************

\parskip 0pt plus 0pt             % Extra vertical space between paragraphs.
\parindent 1pc                    % Width of paragraph indentation.
\topsep 8pt plus 2pt minus 4pt    % Extra vertical space, in addition to
                                  % \parskip, added above and below list and
                                  % paragraphing environments.
\partopsep 2pt plus 1pt minus 1pt % Extra vertical space, in addition to
                                  % \parskip and \topsep, added when user
                                  % leaves blank line before environment.
\itemsep 0pt                      % Extra vertical space, in addition to
                                  % \parskip, added between list items.

% The following page-breaking penalties are defined

\@lowpenalty   51      % Produced by \nopagebreak[1] or \nolinebreak[1]
\@medpenalty  151      % Produced by \nopagebreak[2] or \nolinebreak[2]
\@highpenalty 301      % Produced by \nopagebreak[3] or \nolinebreak[3]

\@beginparpenalty -\@lowpenalty  % Before a list or paragraph environment.
\@endparpenalty   -\@lowpenalty  % After a list or paragraph environment.
\@itempenalty     -\@lowpenalty  % Between list items.

% \clubpenalty         % 'Club line'  at bottom of page.
% \widowpenalty        % 'Widow line' at top of page.
% \displaywidowpenalty % Math display widow line.
% \predisplaypenalty   % Breaking before a math display.
% \postdisplaypenalty  % Breaking after a math display.
% \interlinepenalty    % Breaking at a line within a paragraph.
% \brokenpenalty       % Breaking after a hyphenated line.

%    ****************************************
%    *             SECTIONS                 *
%    ****************************************

% \secdef{UNSTARCMDS}{STARCMDS} :
%    When defining a sectionioning command without using
%    \@startsection, you can use \secdef as follows:
%       \def\part { ... \secdef \CMDA \CMDB }
%       \def\CMDA  [#1]#2{ ... }   % Command to define \part[...]{...}
%       \def\CMDB  #1{ ... }       % Command to define \part*{...}

\def\secshapei{\leftskip-6pc\rightskip3pc plus 1fil \hyphenpenalty2000}

% \@startsection {NAME}{LEVEL}{INDENT}{BEFORESKIP}{AFTERSKIP}{STYLE}
%            optional * [ALTHEADING]{HEADING}
%    Generic command to start a section.
%    NAME       : e.g., 'subsection'
%    LEVEL      : a number, denoting depth of section -- i.e., section=1,
%                 subsection = 2, etc.  A section number will be printed if
%                 and only if LEVEL < or = the value of the secnumdepth
%                 counter.
%    INDENT     : Indentation of heading from left margin
%    BEFORESKIP : Absolute value = skip to leave above the heading.
%                 If negative, then paragraph indent of text following
%                 heading is suppressed.
%    AFTERSKIP  : if positive, then skip to leave below heading,
%                       else - skip to leave to right of run-in heading.
%    STYLE      : commands to set style
%  If '*' missing, then increments the counter.  If it is present, then
%  there should be no [ALTHEADING] argument.  A sectioning command
%  is normally defined to \@startsection + its first six arguments.

\def\section{\@startsection {section}{1}{\z@}{-24pt plus -12pt minus
    -6pt}{8pt plus 3pt minus 2pt}{\secshapei\normalsize\bf}}
\def\subsection{\@startsection{subsection}{2}{\z@}{-18pt plus -6pt minus
   -3pt}{6pt plus 2pt minus 1pt}{\rightskip3pc plus1fil\hyphenpenalty2000
   \large\it}}
\def\subsubsection{\@startsection{subsubsection}{3}{12pt}{-12pt plus
   -6pt minus -2pt}{-6pt}{\normalsize\it}}
\def\paragraph{\@startsection
     {paragraph}{4}{\z@}{3pt plus 1.5pt minus .5pt}{-1em}{\normalsize\bf}}
\def\subparagraph{\@startsection
     {subparagraph}{4}{\parindent}{3pt plus 1.5pt minus
     .5pt}{-1em}{\normalsize\bf}}
\def\@startsection#1#2#3#4#5#6{\if@noskipsec \leavevmode \fi
   \par \@tempskipa #4\relax
   \@afterindenttrue
   \ifdim \@tempskipa <\z@ \@tempskipa -\@tempskipa \@afterindentfalse\fi
   \if@nobreak \everypar{}\else
     \addpenalty{\@secpenalty}\addvspace{\@tempskipa}\fi \@ifstar
     {\@ssect{#3}{#4}{#5}{#1}}{\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}}

\def\@sect#1#2#3#4#5#6[#7]#8{\ifnum #2>\c@secnumdepth
     \def\@svsec{}\else
     \refstepcounter{#1}
     \edef\@svsec{\expandafter\relax\csname @pre#1\endcsname}\fi
     \@tempskipa #5\relax
      \ifdim \@tempskipa>\z@
        \begingroup \expandafter\relax\csname @#1style\endcsname\relax
          \@hangfrom{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par}
        \endgroup
       \csname #1mark\endcsname{#7}\addcontentsline
         {toc}{#1}{\ifnum #2>\c@secnumdepth \else
                      \protect\numberline{\csname the#1\endcsname}\fi
                    #7}\else
        \def\@svsechd{%
            \expandafter\relax\csname @#1style\endcsname\relax
            \hskip #3\@svsec #8\csname #1mark\endcsname
                      {#7}\addcontentsline
                           {toc}{#1}{\ifnum #2>\c@secnumdepth \else
                             \protect\numberline{\csname the#1\endcsname}\fi
                       #7}}\fi
     \@xsect{#5}}

\def\@ssect#1#2#3#4#5{\@tempskipa #3\relax
   \ifdim \@tempskipa>\z@
     \begingroup \expandafter\relax\csname @#4style\endcsname\relax
     \@hangfrom{\hskip #1}{\interlinepenalty \@M #5\par}\endgroup
   \else \edef\@svsechd{\expandafter\relax\csname @#4style\endcsname\relax
         \hskip #1\relax #5}\fi
    \@xsect{#3}}

\def\mysection#1#2#3{
     \expandafter\def\csname @#1style\endcsname{#2}
     \expandafter\def\csname @pre#1\endcsname{#3}}

\mysection{section}{\normalsize\bf}{\hskip-3pc\thesection.\hskip 5pt}
\mysection{subsection}{\large\it}{\thesubsection.\hskip .5em}
\mysection{subsubsection}{\normalsize\it}{\thesubsubsection.\hskip .5em}
\mysection{paragraph}{\normalsize\it}{\theparagraph.\hskip .5em}
\mysection{subparagraph}{\normalsize\it}{\thesubparagraph.\hskip .5em}

% Default initializations of \...mark commands.  (See below for their
% use in defining page styles.

% \def\sectionmark#1{}       % Preloaded definitions
% \def\subsectionmark#1{}
% \def\subsubsectionmark#1{}
% \def\paragraphmark#1{}
% \def\subparagraphmark#1{}

% The value of the counter secnumdepth gives the depth of the
% highest-level sectioning command that is to produce section numbers.

\setcounter{secnumdepth}{3}

% APPENDIX
% The \appendix command must do the following:
%    -- reset the section and subsection counters to zero
%    -- redefine the section counter to produce appendix numbers
%    -- redefine the \section command if appendix titles and headings are
%       to look different from section titles and headings.

\def\appendix{\par
  \setcounter{section}{0}
  \setcounter{subsection}{0}
  \def\thesection{\Alph{section}}}

%    ****************************************
%    *                LISTS                 *
%    ****************************************

% The following commands are used to set the default values for the list
% environment's parameters. See the LaTeX manual for an explanation of
% the meanings of the parameters.  Defaults for the list environment are
% set as follows.  First, \rightmargin, \listparindent and \itemindent
% are set to 0pt.  Then, for a Kth level list, the command \@listK is
% called, where 'K' denotes 'i', 'ii', ... , 'vi'.  (I.e., \@listiii is
% called for a third-level list.)  By convention, \@listK should set
% \leftmargin to \leftmarginK.
% For efficiency, level-one list's values are defined at top level, and
% \@listi is defined to set only \leftmargin

\leftmargini 30pt
\leftmarginii 20pt     % > \labelsep + width of '(m)'
\leftmarginiii 18.7pt  % > \labelsep + width of 'vii.'
\leftmarginiv 17pt     % > \labelsep + width of 'M.'
\leftmarginv 10pt
\leftmarginvi 10pt

%\leftmargin\leftmargini
\leftmargin3pc
\labelsep 8pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\parsep 0pt

\def\@listi{\leftmargin\leftmargini}

\def\@listii{\leftmargin\leftmarginii
   \labelwidth\leftmarginii\advance\labelwidth-\labelsep
   \topsep 4pt plus 2pt minus 1pt
   \parsep 0pt
   \itemsep \parsep}

\def\@listiii{\leftmargin\leftmarginiii
    \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
    \topsep 2pt plus 1pt minus 1pt
    \parsep \z@ \partopsep 1pt plus 0pt minus 1pt
    \itemsep \topsep}

\def\@listiv{\leftmargin\leftmarginiv
     \labelwidth\leftmarginiv\advance\labelwidth-\labelsep}

\def\@listv{\leftmargin\leftmarginv
     \labelwidth\leftmarginv\advance\labelwidth-\labelsep}

\def\@listvi{\leftmargin\leftmarginvi
     \labelwidth\leftmarginvi\advance\labelwidth-\labelsep}

%  Two-side or one-side printing.

% \@twosidefalse               %  Default is one-sided printing.
\def\ds@twoside{\@twosidetrue  %  Defines twoside option.
           \@mparswitchtrue}   %    Marginpars go on outside of page.
%  draft option

% \overfullrule = 0pt             % Default is don't mark overfull hboxes.
\def\ds@draft{\overfullrule 5pt}  % Causes overfull hboxes to be marked.

% The \@options command causes the execution of every command \ds@FOO
% which is defined and for which the user typed the FOO option in his
% \documentstyle command.  For every option BAR he typed for which
% \ds@BAR is not defined, the file BAR.sty will be read after the present
% (main) .STY file is executed.

\@options

%    ****************************************
%    *                LISTS                 *
%    ****************************************

% ENUMERATE
%  Enumeration is done with four counters: enumi, enumii, enumiii
%  and enumiv, where enumN controls the numbering of the Nth level
%  enumeration.  The label is generated by the commands \labelenumi
%  ... \labelenumiv.  The expansion of \p@enumN\theenumN defines the
%  output of a \ref command.

\def\labelenumi{{\theenumi.}}
\def\theenumi{\arabic{enumi}}

\def\labelenumii{{(\alph{enumii})}}
\def\theenumii{\alph{enumii}}
\def\p@enumii{\theenumi}

\def\labelenumiii{\roman{enumiii}.}
\def\theenumiii{\roman{enumiii}}
\def\p@enumiii{\theenumi(\theenumii)}

\def\labelenumiv{\Alph{enumiv}.}
\def\theenumiv{\Alph{enumiv}}
\def\p@enumiv{\p@enumiii\theenumiii}

% ITEMIZE
% Itemization is controlled by four commands: \labelitemi, \labelitemii,
% \labelitemiii, and \labelitemiv, which define the labels of the various
% itemization levels.

\def\labelitemi{$\bullet$}
\def\labelitemii{\bf --}
\def\labelitemiii{$\ast$}
\def\labelitemiv{$\cdot$}

% VERSE
%   The verse environment is defined by making clever use of the
%   list environment's parameters.  The user types \\ to end a line.
%   This is implemented by \let'in \\ equal \@centercr.

\def\verse{\let\\=\@centercr
  \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
          \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
\let\endverse\endlist

% QUOTATION
%   Fills lines
%   Indents paragraph

\def\quotation{\list{}{\listparindent 1.5em
    \itemindent\listparindent
    \rightmargin\leftmargin \parsep 0pt plus 1pt}\item[]}
\let\endquotation=\endlist

% QUOTE -- same as quotation except no paragraph indentation,

\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

% DESCRIPTION

%  To change the formatting of the label, you must redefine
%  \descriptionlabel.

\def\descriptionlabel#1{\hspace\labelsep \bf #1}
\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
       \let\makelabel\descriptionlabel}}

\let\enddescription\endlist

%\newdimen\descriptionmargin
%\descriptionmargin=3em

%    ****************************************
%    *         OTHER ENVIRONMENTS           *
%    ****************************************

% THEOREM
% \@begintheorem ... \@endtheorem are the commands executed at the
% beginning and end of a (user-defined) theorem-like environment.
% Except \@opargbegintheorem is executed when an optional argument is
% given.  Cf. LATEX.TEX.

\def\@begintheorem#1#2{\medbreak\bgroup
   \list{}{\it \leftmargin1pc\labelsep6pt\itemindent0pt
   \item[\indent\hskip3pt{\it #1\ #2.}]}}
\def\@opargbegintheorem#1#2#3{\bgroup\medbreak
   \list{}{\it \leftmargin1pc\labelsep6pt\itemindent0pt
   \item[\indent\hskip3pt\relax{{\it #1\ #2\ (#3).}}]}}
\def\@endtheorem{\endlist\egroup\medskip}

\def\proof{\par\noindent\normalsize{\sc Proof}.\enskip\rm }
% EQUATION and EQNARRAY

%  \newcounter{equation}
%  Default is for left-hand side of equations to be flushleft.
%  To make them flushright, do:
%  \let\@eqnsel = \hfil

\def\theequation{\arabic{equation}}

% \jot = 3pt  % Extra space added between lines of an eqnarray environment

% The macro \@eqnnum defines how equation numbers are to appear in equations.

% \def\@eqnnum{(\theequation)}

% TITLEPAGE
%  In the normal environments, the titlepage environment does nothing but
%  start and end a page, and inhibit page numbers.  It also resets the
%  page number to zero.

%\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
%     \else \newpage \fi \thispagestyle{empty}\c@page\z@}

%\def\endtitlepage{\if@restonecol\twocolumn \else \vskip{12pt} \fi}

\def\ps@myfirstheading{\let\@mkboth\@gobbletwo\topmargin\emptyfoot
\def\@evenfoot{}\def\@oddfoot{\hspace*{0pc}\vtop{\hsize30pc\noindent{\small\it
THE JOURNAL OF LOGIC PROGRAMMING}\vskip6pt\footnotesize\noindent
          \copyright Elsevier Science Publishing Co., Inc., 1993\\
          655 Avenue of the Americas, New York, NY 10010\hfill
          0743-1066/93/\$3.50}}%
\def\@evenhead{}
\def\@oddhead{\hss\vbox{\hsize\fullwidth\hrule\vskip2pt
    \hbox to\fullwidth{\hfill{\footnotesize\rm\uppercase{J. LOGIC
    PROGRAMMING 1993:12:\thepage
    --199}\makebox[3pc][r]{\small\rm\thepage}}}}}}

\long\def\main#1#2{%
 \thispagestyle{myfirstheading}
 \vspace*{6pt}
 \longhrule
 \vspace*{6pt}
 {\leftskip-3pc\rightskip3pc plus1fil\hyphenpenalty2000
 \Large\noindent\bf #1\par}
 \vskip8pc
 {\leftskip-3pc\rightskip3pc plus1fil\hyphenpenalty2000
 \large\noindent\bf #2\par}
 \vskip12pt\relax
 \longhrule}

\pagestyle{myheadings}
%\def\thefootnote{\fnsymbol{footnote}}

%\long\def\author#1{\par\vspace*{-10pt}{\begin{center}\Large\bf
%                                    #1\end{center}}}
%\long\def\and{\par\vspace{6pt}}
%\long\def\affil#1{\par\vspace*{-13pt}{\begin{center}\large\it
% #1\end{center}}\vspace*{13pt}}
%\def\submit#1{\par\vspace{22pt}\noindent{\footnotesize\rm Submitted by #1}}

% ARRAY AND TABULAR

\arraycolsep 5pt % Half the space between columns in an array environment.
\tabcolsep 6pt   % Half the space between columns in a tabular environment.
\arrayrulewidth .4pt % Width of rules in array and tabular environment.
\doublerulesep 2pt   % Space between adjacent rules in array or tabular env.

% TABBING

\tabbingsep \labelsep   % Space used by the \' command.  (See LaTeX manual.)

% MINIPAGE
%  \@minipagerestore is called upon entry to a minipage environment to
%  set up things that are to be handled differently inside a minipage
%  environment. In the current styles, it does nothing.

% \skip\@mpfootins : plays same role for footnotes in a minipage as
%                    \skip\footins does for ordinary footnotes

\skip\@mpfootins = \skip\footins

% FRAMEBOX

\fboxsep = 3pt    % Space left between box and text by \fbox and \framebox.
\fboxrule = .4pt  % Width of rules in box made by \fbox and \framebox.

%    ****************************************
%    *             SECTIONS                 *
%    ****************************************

% DEFINE COUNTERS:

% \newcounter{NEWCTR}[OLDCTR] : Defines NEWCTR to be a counter, which is
%                               reset to zero when counter OLDCTR is stepped.
%                               Counter OLDCTR must already be defined.

%\newcounter {part}
%\newcounter {section}
%\newcounter {subsection}[section]
%\newcounter {subsubsection}[subsection]
%\newcounter {paragraph}[subsubsection]
%\newcounter {subparagraph}[paragraph]

% For any counter CTR, \theCTR is a macro that defines the printed version
% of counter CTR.  It is defined in terms of the following macros:

%  \arabic{COUNTER} : The value of COUNTER printed as an arabic numeral.
%  \roman{COUNTER}  : Its value printed as a lower-case roman numberal.
%  \Roman{COUNTER}  : Its value printed as an upper-case roman numberal.
%  \alph{COUNTER}   : Value of COUNTER printed as a lower-case letter:
%                     1 = a, 2 = b, etc.
%  \Alph{COUNTER}   : Value of COUNTER printed as an upper-case letter:
%                     1 = A, 2 = B, etc.

\def\thepart{\Roman{part}} % Roman numeral part numbers.
\def\thesection       {\arabic{section}}
\def\thesubsection    {\thesection.\arabic{subsection}}
\def\thesubsubsection {\thesubsection .\arabic{subsubsection}}
\def\theparagraph     {\thesubsubsection.\arabic{paragraph}}
\def\thesubparagraph  {\theparagraph.\arabic{subparagraph}}

%    ****************************************
%    *         TABLE OF CONTENTS, ETC.      *
%    ****************************************

% A \subsection command writes a
%       \contentsline{subsection}{TITLE}{PAGE}
% command on the .toc file, where TITLE contains the contents of the
% entry and PAGE is the page number.  If subsections are being numbered,
% then TITLE will be of the form
%       \numberline{NUM}{HEADING}
% where NUM is the number produced by \thesubsection.  Other sectioning
% commands work similarly.

% A \caption command in a 'figure' environment writes
% \contentsline{figure}{\numberline{NUM}{CAPTION}}{PAGE}
% on the .lof file, where NUM is the number produced by \thefigure and
% CAPTION is the figure caption.  It works similarly for a 'table'
% environment.

% The command \contentsline{NAME} expands to \l@NAME.  So, to specify
% the table of contents, we must define \l@section,
% \l@subsection, ... ; to specify the list of figures, we must define
% \l@figure; and so on.  Most of these can be defined with the
% \@dottedtocline command, which works as follows.

% \@dottedtocline{LEVEL}{INDENT}{NUMWIDTH}{TITLE}{PAGE}
%    LEVEL    : An entry is produced only if LEVEL < or = value of
%               'tocdepth' counter.  Note that \section is level 1,
%               \subsection is level 2, etc.
%    INDENT   : The indentation from the outer left margin of the start of
%               the contents line.
%    NUMWIDTH : The width of a box in which the section number is to go,
%               if TITLE includes a \numberline command.

% This command uses the following three parameters, which are set
% with a \def (so em's can be used to make them depend upon the font).
%   \@pnumwidth : The width of a box in which the page number is put.
%   \@tocrmarg  : The right margin for multiple line entries.  One
%                 wants \@tocrmarg > or = \@pnumwidth
%   \@dotsep    : Separation between dots, in mu units.  Should be \def'd to
%                 a number like 2 or 1.7

\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}

%    ****************************************
%    *             BIBLIOGRAPHY             *
%    ****************************************

% The thebibliography environment executes the following commands:

%  \def\newblock{\hskip .11em plus .33em minus .07em} --
%      Defines the `closed' format, where the blocks (major units of
%      information) of an entry run together.

%  \sloppy  -- Used because it's rather hard to do line breaks in
%      bibliographies,

%  \sfcode`\.=1000\relax --
%      Causes a `.' (period) not to produce an end-of-sentence space.

\def\thebibliography#1{%
% \section*{REFERENCES\@mkboth{REFERENCES}{REFERENCES}}\list
 \section*{REFERENCES}\list
  {\small\arabic{enumi}.}{\small\settowidth\labelwidth{#1.\quad}\leftmargin
    \labelwidth\advance\leftmargin\labelsep
    \usecounter{enumi}}
    \def\newblock{\hskip .11em plus .33em minus .07em}
    \sloppy\clubpenalty4000\widowpenalty4000
    \sfcode`\.=1000\relax}

\let\endthebibliography=\endlist

% \def\@biblabel#1{[#1]\hfill}  % Produces the label for a \bibitem[...]
  \def\@biblabel#1{\hfill[#1.]} % Produces the label for a \bibitem[...]
                                % command.
% \def\@cite#1{[#1]}            % Produces the output of the \cite command.

%    ****************************************
%    *             FOOTNOTES                *
%    ****************************************

% \footnoterule is a macro to draw the rule separating the footnotes from
% the text.  It should take zero vertical space, so it needs a negative
% skip to compensate for any positive space taken by the rule.  (See
% PLAIN.TEX.)

\def\footnoterule{\kern-3\p@
  \hrule width 6pc
  \kern 2.6\p@}                 % The \hrule has default height of .4pt .
\def\footnoterule{\kern-3\p@
  \hspace*{-3pc}\vrule height.4pt depth0pt width9pc\endgraf
  \kern 2.6\p@}                 % The \hrule has default height of .4pt .

% \newcounter{footnote}

% The numbering style (arabic, alph, etc.) for ordinary footnotes
% is defined by the macro \thefootnote.

%   \@makefntext{NOTE} :
%        Must produce the actual footnote, using \@thefnmark as the mark
%        of the footnote and NOTE as the text.  It is called when effectively
%        inside a \parbox of width \columnwidth (i.e., with \hsize =
%        \columnwidth).

%        The following macro indents all lines of the footnote by 10pt, and
%        indents the first line of a new paragraph by 1em.  To change these
%        dimensions, just substitute the desired value for '10pt' [in both
%        places] or '1em'.  The mark is flushright against the footnote.
%          \long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
%             \advance\@tempdima-10pt\parshape \@ne 10pt \@tempdima}\par
%             \parindent 1em\noindent \hbox to \z@{\hss$^{\@thefnmark}$}#1}

%        A simpler macro is used, in which the footnote text is
%        set like an ordinary text paragraph, with no indentation except
%        on the first line of a paragraph, and the first line of the
%        footnote.  Thus, all the macro must do is set \parindent
%        to the appropriate value for succeeding paragraphs and put the
%        proper indentation before mark.

\long\def\@makefntext#1{\parindent 0pt\hspace{10pt}
            \hbox{$^{\@thefnmark}$}#1}
%\def\@xfootnotemark[#1]{\begingroup \c@footnote #1\relax
%    \xdef\@thefnmark{\thefootnote}\endgroup \@footnotemark}

%\def\@makefnmark{\hbox to 0pt{$^{\@thefnmark}$\hss}}
%\def\@footnotemark{\leavevmode\ifhmode
%    \edef\@x@sf{\the\spacefactor}\fi \@makefnmark
%    \ifhmode\spacefactor\@x@sf\fi\relax}

%\def\footnote{\@ifnextchar[{\@xfootnote}{\stepcounter
%   {\@mpfn}\xdef\@thefnmark{\thempfn}\@footnotemark
%   \@footnotetext}}

\def\thanksone#1{\renewcommand{\thefootnote}{\fnsymbol{footnote}}
\footnote{#1}\renewcommand{\thefootnote}{\arabic{footnote}}
\setcounter{footnote}{0}}

\def\thankstwo#1{\addtocounter{footnote}{1}\renewcommand{\thefootnote}%
{\fnsymbol{footnote}}\footnote{#1}
\renewcommand{\thefootnote}{\arabic{footnote}}\setcounter{footnote}{0}}

\def\thanksthree#1{\addtocounter{footnote}{2}\renewcommand{\thefootnote}%
{\fnsymbol{footnote}}\footnote{#1}\renewcommand{\thefootnote}{%
\arabic{footnote}}\setcounter{footnote}{0}}

\gdef\affil#1{\renewcommand{\thefootnote}{}\footnote{{\footnotesize\it
Address correspondence to\/}#1}\renewcommand{\thefootnote}%
{\arabic{footnote}}\setcounter{footnote}{0}}

\gdef\rec#1#2{\renewcommand{\thefootnote}{}\footnote{Received
#1; accepted #2.}\renewcommand{\thefootnote}{\arabic{footnote}}
\setcounter{footnote}{0}}

% \@makefnmark : A macro to generate the footnote marker that goes
%                in the text.  Default definition used.

%    ****************************************
%    *         FIGURES AND TABLES           *
%    ****************************************

% Float placement parameters.  See LaTeX manual for their definition.

\setcounter{topnumber}{2}
\def\topfraction{.7}
\setcounter{bottomnumber}{1}
\def\bottomfraction{.3}
\setcounter{totalnumber}{3}
\def\textfraction{.2}
\def\floatpagefraction{.5}
\setcounter{dbltopnumber}{2}
\def\dbltopfraction{.7}
\def\dblfloatpagefraction{.5}

% \@makecaption{NUMBER}{TEXT} : Macro to make a figure or table caption.
%      NUMBER : Figure or table number--e.g., 'Figure 3.2'
%      TEXT   : The caption text.
% Macro should be called inside a \parbox of right width, with \normalsize.
% changed 25 Jun 86 to fix according to Howard Trickey:
% instead of \unhbox\@tempboxa\par we do #1: #2\par

\long\def\@makecaption#1#2{
   \vskip 10pt
   \setbox\@tempboxa\hbox{{\small{\bf #1.}\ {\rm #2}}}
   \ifdim \wd\@tempboxa >\hsize   % IF longer than one line:
       {\small{\bf #1.} {\rm #2}}\par %   THEN set as ordinary paragraph.
     \else                        %   ELSE  center.
       \hbox to\hsize{\hfil\box\@tempboxa\hfil}  
   \fi}

% To define a float of type TYPE (e.g., TYPE = figure), the document style
% must define the following.

%  \fps@TYPE   : The default placement specifier for floats of type TYPE.

%  \ftype@TYPE : The type number for floats of type TYPE.  Each TYPE has
%                associated a unique positive TYPE NUMBER, which is a power
%                of two.  E.g., figures might have type number 1, tables type
%                number 2, programs type number 4, etc.

%  \ext@TYPE   : The file extension indicating the file on which the
%                contents list for float type TYPE is stored.  For example,
%                \ext@figure = 'lof'.

%  \fnum@TYPE  : A macro to generate the figure number for a caption.
%                For example, \fnum@TYPE == Figure \thefigure.

%  The actual float-making environment commands--e.g., the commands
%  \figure and \endfigure--are defined in terms of the macros \@float
%  and \end@float, which are described below.

%  \@float{TYPE}[PLACEMENT] : Macro to begin a float environment for a
%     single-column float of type TYPE with PLACEMENT as the placement
%     specifier.  The default value of PLACEMENT is defined by \fps@TYPE.
%     The environment is ended by \end@float.
%     E.g., \figure == \@float{figure}, \endfigure == \end@float.

% FIGURE

%\newcounter{figure}
\def\thefigure{\@arabic\c@figure}

\def\fps@figure{tbp}
\def\ftype@figure{1}
\def\ext@figure{lof}
\def\fnum@figure{Figure \thefigure}
\def\figure{\@float{figure}}
\let\endfigure\end@float
\@namedef{figure*}{\@dblfloat{figure}}
\@namedef{endfigure*}{\end@dblfloat}

% TABLE

%\newcounter{table}
\def\thetable{\@arabic\c@table}

\def\fps@table{tbp}
\def\ftype@table{2}
\def\ext@table{lot}
\def\fnum@table{Table \thetable}
\def\table{\@float{table}}
\let\endtable\end@float
\@namedef{table*}{\@dblfloat{table}}
\@namedef{endtable*}{\end@dblfloat}

%    ****************************************
%    *         TITLE AND ABSTRACT           *
%    ****************************************

% \maketitle ==
%  BEGIN
%    \par
%    \begingroup
%      redefine \@makefnmark so footnote marks take zero space (this make
%        centering look better)
%      \thefootnote == \fnsymbol{footnote} % to number by *, dagger, etc.
%      if @twocolumn = true
%        then  \twocolumn[\@maketitle]
%        else \@maketitle
%      fi
%   \thispagestyle{plain}
%   \@thanks % \thanks defines \@thanks to have \footnotetext commands for
%            % producing footnotes.
%   \endgroup
%  END

\def\maketitle{\par
 \begingroup
   \def\thefootnote{\fnsymbol{footnote}}
   \def\@makefnmark{\hbox
       to 0pt{$^{\@thefnmark}$\hss}}
   \if@twocolumn
     \twocolumn[\@maketitle]
     \else \newpage
     \global\@topnum\z@     % Prevents figures from going at top of page.
     \@maketitle \fi\thispagestyle{plain}\@thanks
 \endgroup
 \setcounter{footnote}{0}
 \let\maketitle\relax
 \let\@maketitle\relax
 \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\let\thanks\relax}

\def\@maketitle{\newpage
 \null
 \vskip 0em              % Vertical space above title.
 \begin{center}\Huge
 \@title\end{center}     % Title set in \Huge size.
  \vskip 12pt            % Vertical space after title.
  {\begin{center}\Large  % each author set in \Large,
   \lineskip .5em
   \end{center}}
  \vskip 4pt             % Vertical space after author.
 \par
 \vskip 27pt}            % Vertical space after date.

%\def\abstract{\vspace*{1.2pc}\bgroup\everypar={\rightskip3pc}\normalsize
%              \noindent\kern-3pc\makebox[3pc][l]{$\rhd$}\ignorespaces }
%\def\endabstract{\hfill$\lhd${\kern-3pc}\egroup\vspace*{.5pc}\longhrule}

\def\abstract{\vspace*{.8pc}\begin{list}{}{\normalsize
               \leftmargin0pc\rightmargin3pc}
               \item\hspace*{-3pc}\makebox[3pc][l]{$\rhd$}\ignorespaces }
\def\endabstract{\hfill$\lhd${\kern-3pc}\end{list}\vspace*{.2pc}\longhrule}

\mark{{}{}}   % Initializes TeX's marks

%\if@twoside         % If two-sided printing.
%\def\ps@headings{\let\@mkboth\markboth
%\def\@oddfoot{}\def\@evenfoot{}%   No feet.
%\def\@evenhead{\rm \thepage\hfil \uppercase{\leftmark}}% Left heading.
%\def\@oddhead{\hbox{}\uppercase{\rightmark}\hfil \rm\thepage}% Right heading.
%\def\sectionmark##1{\markboth {\uppercase{\ifnum \c@secnumdepth >\z@
%    \thesection\hskip 1em\relax \fi ##1}}{}}%
%\def\subsectionmark##1{\markright {\ifnum \c@secnumdepth >\@ne
%          \thesubsection\hskip 1em\relax \fi ##1}}}
%\else               % If one-sided printing.
%\def\ps@headings{\let\@mkboth\markboth
%\def\@oddfoot{}\def\@evenfoot{}%     No feet.
%\def\@evenhead{\rm \thepage\hfil \uppercase{\leftmark}}% Left heading.
%\def\@oddhead{\hbox {}\uppercase{\rightmark} \hfil \rm\thepage}% Heading.
%\def\sectionmark##1{\markright {\uppercase{\ifnum \c@secnumdepth >\z@
%    \thesection\hskip 1em\relax \fi ##1}}}}
%\fi

% Definition of 'myheadings' page style.

\def\ps@myheadings{\let\@mkboth=\markboth
 \topmargin\emptyfoot
 \def\@evenfoot{}\def\@oddfoot{} % empty feet
 \def\@evenhead{\hss\vbox{\hsize\fullwidth\hrule\vskip2pt
                \hbox to\fullwidth{{\small\rm\thepage\hfil
                \uppercase{\leftmark}}}}}
 \def\@oddhead{\hss\vbox{\hsize\fullwidth\hrule\vskip2pt
                \hbox to\fullwidth{{\small\rm\uppercase{\rightmark}\hfil
                \thepage}}}}}

\pagestyle{myheadings}

% DATE

\def\today{\ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \space\number\day, \number\year}

%    ****************************************
%    *           INITIALIZATION             *
%    ****************************************

% Default initializations

\ps@myheadings                   % page style
\pagenumbering{arabic}           % Arabic page numbers
\onecolumn                       % Single-column.
\if@twoside\else\raggedbottom\fi % Ragged bottom unless twoside option.
