\documentclass{jfrarticle}

% syntax: \title[short title]{very very very very long title}
% the long title is mandatory and will appear in the title page
% the short title is optional and is used inside the headings; if it is not specified, the long title will be
% used instead
\title{Reasoning on Formal Reasoning}

% syntax: \author{short authors}{full authors}
% the first parameter is the list of the (first) authors and is used inside the headings; 
% the second one is the full list of authors, including their affiliations, and is shown in the title page
\author{Testone Miller et al.}
{TESTONE MILLER\\Head of the Department of Bribing Sciences, University of Calisota\\
GERONIMO MAYALL\\Megasoft Research \and
WINSTON SMITH\\Minister of Truth, Oceania}
\begin{abstract}
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
\end{abstract}

\begin{document}
\setcounter{page}{1}
\firstfoot{Journal of Formalized Reasoning  Vol.??, No.??, ??, Pages \pages.}
\runningfoot{Journal of Formalized Reasoning Vol.??, No.??, ??}


\maketitle

\section{Introduction}

This article is a description of the \LaTeX\ {\tt jfrarticle} document
style for typesetting articles in the format of the Journal of Formal Reasoning (which is a stripped down version of the ACM transactions style). It has, of
course, been typeset using this document style, so it is a
self-illustrating article.  The reader is assumed to be familiar
with \LaTeX.

The preferred bibliography style is the {\tt alpha} style, using BibTeX.

\LaTeX\ is a document preparation system
implemented as a macro package in Donald Knuth's
\TeX\ typesetting system.  It is based
upon the premise that the user should describe the logical structure of
his document and not how the document is to be formatted.  Formatting
is under the direction of a {\em document style} chosen by the user.
The user can dramatically change the way the document is formatted by
simply choosing a different document style.  

It is impossible to provide predefined logical structures to handle all
situations that may arise in a document, so users must sometimes make
their own formatting decisions.  \LaTeX\ provides a number of features
to assist in this task and, if necessary, the user can call upon the
full power of \TeX, which is probably the most powerful typesetting
system currently available.  

\section{The Title Page}

\subsection{The Title, Author(s), and Abstract}

Following order is mandatory to generate a correct title page:

\begin{verbatim}
		      \documentstyle{jfrarticle}
		      \title{}
		      \author{}{}
		      \begin{abstract} ...  \end{abstract}
		      \begin{document}
		      \begin{bottomstuff} ... \end{bottomstuff}
		      \maketitle
\end{verbatim}

\subsubsection{Title and Author}
The \LaTeX\ \verb|\title| and \verb|\author| declarations and the
\verb|\maketitle| command are similar to the usual ones, with some peculiarities.
The \verb|\title| declaration allows one optional parameter containing a short title, to be used in the headings of the article. The \verb|\author| declaration requires two parameters, the first being the list of the authors in short, and the second one being the full list of authors, including their affiliation. The short list must be specified as follows:

\begin{itemize}
\item If there is one author, then use author's full name (ex. Leslie Lamport);
\item If there are two authors, then abbreviate each author's first name
           (L.~Lamport and A.~Appel);
\item If there are more than two authors, then the format is Leslie Lamport et al.
\end{itemize}

The full list must follow the format illustrated in the following example:

\begin{quote}
\begin{verbatim}
\author{J.~E.~Archer, jr. et al.}
        {JAMES E. ARCHER, JR.\\ Rational Machines
        \and RICHARD CONWAY and FRED B. SCHNEIDER \\ 
             Cornell University}
\end{verbatim}
\end{quote}
Note that authors' names are in uppercase letters, authors are
separated from their affiliation by a \verb|\\| command, multiple
authors with the same affiliation are separated by ``and'' (or commas
and ``and'' if there are more than two), and authors with different
affiliations are separated by an \verb|\and| command.  The following
example shows what to do if there are more than
two affiliations:
\begin{quote}
\begin{verbatim}
\author{E.~Korach et al.}
        {E. KORACH \\ IBM Israel \\
        D. ROTEM \\ University of Waterloo
        \and N. SANTORO \\ Carleton University}
\end{verbatim}
\end{quote}
In both the title and the author, you may have to insert \verb|\\|
commands if lines need to be broken.

\subsubsection{Abstract}
The abstract is typed as usual with the {\tt abstract} environment.
However, this environment must come before the \verb|\maketitle|
command.


\section{Ordinary Text}

Most of the body of the text is typed just as in an ordinary
document.  This section lists the differences.

\subsection{Lists}

\subsubsection{Enumeration and Itemization}

Let's begin with enumeration.
\begin{longenum}
\item The style has two different formats for 
itemized lists, which I will call the {\em long\/} and {\em short\/}
formats. This list is an example of the long format.

\item The ordinary {\tt enumerate} environment
produces the short format.  For the long format, use the
{\tt longenum} environment.
\begin{enumerate}\itemindent 10pt
\item This inner enumeration uses the short format.
\item It was produced using \LaTeX's ordinary {\tt enumerate}
      environment.
\item there is no standard for enumerations nested more than
      two levels deep.
\end{enumerate}
\end{longenum}

Itemized lists are similar to enumerated ones.
\begin{longitem}
\item As with enumerations, there is a long and a short
format for itemized lists.  This list is in the long format.

\item The long format is produced by the {\tt longitem}
environment.  The ordinary {\tt itemize} environment
uses the short format.
\begin{itemize}
\item This is an itemized list using the short format.

\item It was produced  with the {\tt itemize} environment
that is used in ordinary \LaTeX\ input.
\end{itemize}
\end{longitem}

It is interesting to observe that the style of tick mark used
for an itemization changed around 1985 from an en dash
(--) to an em dash (---). % jtb: changed!

\subsubsection{Descriptions}

A list is a sequence of displayed text elements, called items, each
composed of the following two elements:
\begin{describe}{{\em item body\/}:}
\item[{\em label\/}:]
A marker that identifies or sets off the item.  It
is a number in an enumerated list and a tick mark in an itemized list.

\item[{\em item body\/}:] The text of the item.  It is usually ordinary prose,
but sometimes consists of an equation, a program statement, etc.

Or another paragraph, which will be indented like normal paragraphs.
\end{describe}

When the labels of a list are names rather than numbers or tick marks,
the list is called a {\em description\/} list.
There are both long and short description lists.  The above list is a short
description list; the bodies of all the items are indented enough to
accommodate the widest label.
The following list is a long description list.
The {\tt acmtrans} style provides both kinds of description lists:
\begin{description}
\item[short]
The {\tt describe} environment 
%that works the
%same as the {\tt description} environment except that it 
takes an argument, which should be the same as the argument of the \verb|\item|
command that produces the widest label.  Thus, the above description
list was begun with the command
\begin{quote}
\begin{verbatim}
\begin{describe}{{\em item body\/}:}
\end{verbatim}
\end{quote}

A description label is often emphasized in some way; in this example I
used the \LaTeX\ \verb|\em| command, italicized the label. 
An \verb|\hfill| command can be used to produce
a label like ``{\em gnu \hfill --\/}'' where {\em gnu\/} is flush left
against the margin and the ``--'' is aligned flush right next to the
item body.

\item[long]
The standard \LaTeX\ {\tt description} environment produces a long
description list.  It italicizes the labels, and puts a period after
them.
\end{description}

\subsection{Theorems, Etc.}

%\newtheorem{theorem}{Theorem}[subsection]
%\begin{theorem}
%testing section counter
%\end{theorem}

\LaTeX\ provides a single class of theorem-like environments, which are
defined with the \verb|\newtheorem| command.  The
style divides this class into two subclasses that are formatted
differently.  The first class includes theorems, corollaries, lemmas,
and propositions.  It is produced with the \verb|\newtheorem| command.
Such a theorem-like environment is often followed by a proof, for which
the {\tt acmtrans} style provides a {\tt proof} environment.

\newtheorem{subtheorem}{Theorem}[subsection]
\begin{subtheorem}
Notice that theorems are numbered inside the nearest section\newline subsection.
\end{subtheorem}

When listing within the theorem environment, this style will now produce
roman parantheses. Thank you David Sands.

\begin{proof}	
This theorem is an instance of {\tt subtheorem}, theorems nested in
subsections.
\end{proof}


The second subclass of theorem-like environments includes ones for
definitions, examples, and remarks.  These environments are defined
with the \verb|\newdef| command, which works the same as
\verb|\newtheorem|.  Here
is an example of such an environment.

\newdef{subexample}[subtheorem]{Definition}

\begin{subexample}
This is an example of a Definition, typed with an {\tt subexample}
environment defined with \verb|\newdef|.
As you can see theorems are italicized and definitions are not.
\end{subexample}

\newtheorem{subproperty}[subtheorem]{Property}

Sometimes theorem-like environments are numbered in unusual ways, or
are identified by a name.  Consider the following example:
\begin{subproperty}[{\rm Ca}]
Let syn $\in$ Syn, occ $\in$ Occ be maximal and sta $\in$ Sta.  Then
Tcol\/{\rm [[}syn\/{\rm ]]} occ sta\hspace{-2pt} $\downarrow\!1$ $=$
Tsto\/{\rm [[}syn\/{\rm ]]} sta.
\end{subproperty}
\begin{proof}[of Property {\rm Ca}]
By straightforward structural induction, and is \linebreak
omitted.
\end{proof}
It was obtained by giving optional arguments to the
{\tt property} environment (defined with \verb|\newtheorem|)
and the {\tt proof} environment and was typed as follows.
\begin{quote}
\begin{verbatim}
\begin{subproperty}[{\rm Ca}] Let ...  \end{subproperty}
\begin{proof}[of Property {\rm Ca}]  By straightforward ...
\end{verbatim}
\end{quote}
Notice that the optional argument to the {\tt property} environment
suppresses the automatic numbering.  If a null optional argument
were given to this environment by typing ``{\tt []}'', then
it would have produced the label ``{\sc Property.}''  This is
how unnumbered theorems, etc.\ are produced.

Environments defined by \verb|\newdef| use the optional
argument the same way as those defined by \verb|\newtheorem|.

\vskip10pt
With this definition

\begin{verbatim}
     \newtheorem{secthm}{Theorem}[section]
\end{verbatim}
\noindent
one can solve the counter problems and counter and label problems for
theorems, lemmas and definitions etc.

With the above definition and with the following variations
\begin{verbatim}
     \newdef{secdefn}[secthm]{Definition} or
     \newdef{seclem}[secthm]{Lemma} or
     \newdef{sectheo}{secthm]{Theorem} etc.
\end{verbatim}
\noindent
one can achieve
\begin{enumerate} 
\item correct counters in definitions, theorems etc. in \verb|\section| environment.
For example, to generate ``Definition 4.1.''; without the above two definitions, it produces ``Definition 4.0.1.'' and
\item correct counter and label associated with definitions, theorems etc. in any environment (section or subsection). For example, 
\begin{verbatim}
     \begin{secdefn}[\thesecthm\ (label)] 
       text text text
     \end{secdefn}
\end{verbatim}
produces the correct definition counter + correct placement of the period as in
``Definition 3.1 (label).''.
\end{enumerate}

\subsection{Overfull hbox - Stretching/filling one horizontal line}

To solve a line break due to ``Overfull \verb|\hbox|'', here is a plain \TeX\ 
solution; here \verb|\hsize| is the default setting of acmtrans.sty:

\begin{center}
\verb|\hbox to \hsize{line sentence to be stretched}|
\end{center}

This can be used in a list environment as well but \verb|\hsize| declared to a reduce
dimension:

\begin{verbatim}
   \hbox{\vbox{\hsize = less than the default setting
   \hbox to \hsize{line sentence to be stretched}}}
\end{verbatim}

\subsection{Programs}

Good formatting of programs requires a knowledge of their semantics,
and is beyond the scope of a document production system.  While
``pretty printers'' are useful for handling the many pages of a real
program, the short examples that are published in articles should be
formatted by hand to improve their clarity.  The \LaTeX\ {\tt tabbing}
environment makes the formatting of programs relatively easy,
especially if the user defines commands for his particular language
constructs.
One may also use the {\tt verbatim} environment.

Programs in running text should be indented two ems 
on each side (as provided by the {\tt quote} environment), and
programs in regular figures should be centered.
(Programs in ``narrow figures'' (q.v.) are left or right justified
automatically).

Here is an example of a program:
\begin{quote}
\begin{tabbing}
{\bf type} date =\\
\hspace*{1em}\= {\bf record} \= day: 1\,.\,.\,31;\+\+\\
                                month: 1\,.\,.\,12;\\
                                year: integer \-\\
                {\bf end} \-\\
{\bf var} mybirth, today : date;\\
{\bf var} myage : integer;
\end{tabbing}
\end{quote}
Figure~\ref{fig:prog} shows how the same program looks in a figure.
\begin{figure}
\centerline{\parbox{104pt}{% it's safe to overestimate the size here
\begin{tabbing}
{\bf type} date =\\
\hspace*{1em}\= {\bf record} \= day: 1\,.\,.\,31;\+\+\\
                                month: 1\,.\,.\,12;\\
                                year: integer \-\\
                {\bf end} \-\\
{\bf var} mybirth, today : date;\\
{\bf var} myage : integer;
\end{tabbing}}}
\caption{An example of a program centered in a figure}
\label{fig:prog}
\end{figure}

In addition to formatting programs, the {\tt tabbing} environment may be
used for similar displayed material such as BNF syntax specifications
and rewrite rules.

\subsection{User-specified Formatting}

If \LaTeX\ does not provide a particular text structure, the user must
define it himself and specify how it is to be formatted.  This is most
easily done by defining the new structure in terms of existing ones;
the \LaTeX\ {\tt list} and {\tt trivlist} environments are useful
tools.  However, it is occasionally necessary for the user to provide
explicit formatting commands.  


\section{Figures and Tables}

\subsection{Figures}

The ordinary \LaTeX\ {\tt figure} environment works as usual.
Figure~\ref{fig:ordinary}, a bogus reference,
\begin{figure}
\centering
\(\begin{array}{c|ccc}
     & \bot & F & T \\
\hline
\bot & \bot & \bot & T \\
F    & \bot & F    & T \\
T    & \bot & T    & T
\end{array}\)
\caption{The truth table for the parallel-or.}
\label{fig:ordinary}
\end{figure}
was produced in this way.
Note that figures should never appear in the text or at the bottom of
a page. (If you use the figure placement optional argument, use only
\verb"t" or \verb"p" or both; do not use \verb"h" or \verb"b").

Some figures (and tables) have no caption except for the figure number.
For such figures (and tables), one uses a \verb|\nocaption| command,
which has no argument, instead of the \verb|\caption| command.

\begin{narrowfig}{3in}
\begin{tabbing}
{\bf type} date =\\
\hspace*{1em}\= {\bf record} \= day: 1\,.\,.\,31;\+\+\\
                                month: 1\,.\,.\,12;\\
                                year: integer \-\\
                {\bf end} \-\\
{\bf var} mybirth, today : date;\\
{\bf var} myage : integer;
\end{tabbing}
\caption{An example of a program displayed in a figure.}
\label{fig:narrow}
\end{narrowfig}

In addition to this method of formatting figures, there are
also figures with side captions, as in Figure~\ref{fig:narrow}.
Such a figure is produced with the {\tt narrowfig} environment.  This
environment has a single mandatory argument, which is the width of the
figure.
Note that if the figure is generated by {\tt tabbing} or {\tt
tabular}, one can safely overestimate the size.
It works just like the ordinary {\tt figure} environment,
except it must contain only one \verb|\caption| or \verb|\nocaption|
command, which must come after the figure itself.  

The {\tt narrowfig} environment should obviously not be used unless the
figure is narrow enough to leave a reasonable amount of space beside it
for the caption.  


\subsection{Tables}

The ordinary \LaTeX\ {\tt table} environment can be used, but it
requires the user to add formatting commands to match the journal
style.  This formatting is performed automatically
if the {\tt acmtable} environment is used instead, producing
the result shown in Table~\ref{tab:table}, which shows the same
table displayed in Figure~\ref{fig:ordinary}.
\begin{acmtable}{100pt}
\centering
\(\begin{array}{c|ccc}
     & \bot & F & T \\
\hline
\bot & \bot & \bot & T \\
F    & \bot & F    & T \\
T    & \bot & T    & T
\end{array}\)
\caption{The truth table for the parallel-or.}
\label{tab:table}
\end{acmtable}
This environment has a mandatory argument that equals the width
of the table---more precisely, it specifies the width of the rules
above and below the table.  There must be only one 
\verb|\caption| or \verb|\nocaption|
command, which must come after the text of the table.  
(Even though the table caption is printed above the table, the
\verb|\caption| command comes after the table in the input file.)


\section{The End of the Document}

\subsection{Appendix}

The appendix (if the article has one) should precede the
acknowledgments (if any) and bibliography.
If the appendix isn't broken into separate sections,
then you should add the following commands after the \verb|\appendix|
command:
\begin{quote}
\begin{verbatim}
\section*{APPENDIX}
\setcounter{section}{1}
\end{verbatim}
\end{quote}
Setting the counter is necessary so that numbered subsections and
theorems will have the names ``A.{\em N\/}'' in the text.

For an article with multiple appendices, one begins
the appendix with an \verb|\appendix| followed by
\verb|\section*{APPENDIX}|, and then starts each
appendix with an ordinary \verb|\section| command.

\subsection{Acknowledgments}

An optional acknowledgments section follows all the text of the
article, including any appendices.  It is produced with the
{\tt acks} environment.  (Since I can never remember how many
{\em e\/}'s there are in {\em acknowledgments}, it seemed
like an abbreviation was in order for the environment name.
One may also spell out the name as {\tt acknowledgments}).
Sometimes, there is just a single acknowledgment.
This may be given using the {\tt ack} or {\tt acknowledgment}
environment.

\subsection{Bibliography}

The bibliography follows the acknowledgments, and is the last
significant body of text in the article.  It is produced by the usual
\LaTeX\ commands. 

Put
\begin{quote}
\begin{verbatim}
\bibliographystyle{alpha}
\bibliography{bibliodb}
\end{verbatim}
\end{quote}
between the \verb|\begin{document}| and the \verb|\end{document}|. {\tt bibliodb} 
refers to the file name of your BibTeX database.

The conventional \verb|\cite| command will generate citations as usual in
\LaTeX.

\section{Running Heads and Feet}

The running foot of all but the title page of the article is declared
with the \linebreak
\verb|\runningfoot| command.  It contains the name of the
journal, volume, number, and date.  The foot for the title page
contains this information plus the page numbers.  It is declared
with the \verb|\firstfoot| command.

The \verb|\pages| command prints the page numbers of the article,
producing something like ``123--132''.  It is implemented with the
\LaTeX\ \verb|\pageref| command, so it will not produce the correct
page numbers the first time the file is run through \LaTeX, or if the
number of the first or last page has changed since the last time.

The default page style for the {\tt acmtrans} style is {\tt
myheadings}.  Thus, a \verb|\markboth| command is used to set the
running heads.  The left head contains the author's name (or authors'
names) and the right head contains the title.  For long titles,
some contraction of the title is used.

\bibliographystyle{alpha}
\bibliography{}

%do not remove
\begin{received}
\end{received}
\end{document}





