new latex package turnstile (7sep07)

git-svn-id: svn://tug.org/texlive/trunk@4917 c570f23f-e606-0410-a88d-b1316a301751

9 files changed, 694 insertions, 0 deletions

diff --git a/Master/texmf-dist/doc/latex/turnstile/README b/Master/texmf-dist/doc/latex/turnstile/README
new file mode 100644
index 00000000000..589409ada58
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/README
@@ -0,0 +1,43 @@
+turnstile
+    This style was based on article.cls to be used for typesetting
+    articles. Among other uses, the turnstile sign is used by logicians
+    for denoting a consequence relation, related to a given logic,
+    between a collection of formulas and a formula. Many logicians
+    have complaint the lack of a LaTeX routine for issuing turnstile
+    signs, in any of the forms it could arise.
+
+AUTHOR
+    Arthur Buchsbaum and Francisco Reinaldo.
+    arthur@inf.ufsc.br, reinaldo.opus@gmail.com
+
+
+COPYRIGHT
+  This program is provided under the terms of the
+  LaTeX Project Public License distributed from CTAN
+  archives in the directory macros/latex/base/lppl.txt.
+  (C) 2007 Arthur Buchsbaum e Francisco Reinaldo
+
+FILES AND DIRECTORIES AT CTAN
+  README            This file
+  turnstile-en\      Directory of turnstile style (English version)
+  turnstile-pt\      Directory of turnstile style (Portuguese version)
+
+:.
+.    README
+.
++---turnstile-pt
+.        README.pt
+.        turnstile-pt.dtx
+.        turnstile-pt.ins
+.        turnstile-pt.pdf
+.        turnstile_artigo.pdf
+.        turnstile_artigo.tex
++---turnstile-en
+.        README.en
+.        turnstile-en.dtx
+.        turnstile-en.ins
+.        turnstile-en.pdf
+.        turnstile_article.pdf
+.        turnstile_article.tex
+        
+Thanks and enjoy it!  
diff --git a/Master/texmf-dist/doc/latex/turnstile/README.en b/Master/texmf-dist/doc/latex/turnstile/README.en
new file mode 100644
index 00000000000..3639e62eba2
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/README.en
@@ -0,0 +1,58 @@
+turnstile
+  This style was based on article.cls to be used for typesetting
+  articles. Among other uses, the turnstile sign is used by logicians
+  for denoting a consequence relation, related to a given logic,
+  between a collection of formulas and a formula. This package aims to
+  issue the turnstile sign in many ways, and is capable of
+  putting labels below and above it.
+
+AUTHOR
+  Arthur Buchsbaum and Francisco Reinaldo.
+  arthur@inf.ufsc.br, reinaldo.opus@gmail.com
+
+
+COPYRIGHT
+  This program is provided under the terms of the
+  LaTeX Project Public License distributed from CTAN
+  archives in the directory macros/latex/base/lppl.txt.
+  (C) 2007 Arthur Buchsbaum e Francisco Reinaldo
+
+VERSION
+  This is the turnstile version 1.0
+
+CHANGES
+  1.0  First public release.
+
+FILES AND DIRECTORIES AT CTAN
+  README.en              This file
+  turnstile-en.dtx       The source of turnstile style
+  turnstile-en.pdf       Pdf version of turnstile style
+  turnstile-en.ins       Driver file for turnstile-en.dtx
+  turnstile_article.tex  Source code of article
+  turnstile_article.pdf  Pdf version of the documentation,
+                         published PracTeX Journal: Issue 2007-3
+
+REQUIREMENTS
+  The installation of the turnstile package requires the ifthen
+  package. Please use <<the last LaTeX version>>.
+
+INSTALLATION (OF THE LATEX PACKAGE AND THE METAFONT SOURCE FILES)
+  The installation procedure is described in the documentation, but
+  you can also follow these steps.
+
+  1. Download the files turnsilte-en\turnstile-en.ins and 
+	 turnsilte-en\turnstile-en.dtx to a preferably
+     empty directory. If you intend to keep the documentation, you'd
+     better create a suitable directory and put the files there right
+     now
+  2. Start a shell where you can enter commands from the keyboard
+  3. Go to the directory where you did put the files turnstile-en.dtx
+     and turnstile-en.ins
+  4. Run the command
+       pdflatex turnstile-en.ins
+     You will obtain the turnstile-en.sty
+  5. Run the command
+       pdflatex turnstile-en.dtx
+     to produce the documentation and test the installation.
+     Run it one more time to resolve the references, before
+     you view it
diff --git a/Master/texmf-dist/doc/latex/turnstile/README.pt b/Master/texmf-dist/doc/latex/turnstile/README.pt
new file mode 100644
index 00000000000..47754a32454
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/README.pt
@@ -0,0 +1,61 @@
+(para compatibilidades com o site CTAN, este arquivo estah formatado em 7bits) 
+
+turnstile
+  Este estilo eh baseado no article.cls, usado para a composicao de
+  artigos. Entre outras utilizacoes, a barra de Frege eh usada
+  pelos logicos para denotar a relacao de consequencia, com
+  respeito a uma dada logica, entre colecoes de formulas e
+  formulas. O pacote turnstile foi feito para desenhar a
+  barra de Frege em varias formas, e para colocar dados abaixo e 
+  acima deste simbolo.
+
+AUTORES
+  Arthur Buchsbaum e Francisco Reinaldo
+  arthur@gmail.com, reinaldo.opus@gmail.com
+
+
+COPYRIGHT
+  Este programa eh provido sob os termos de Licenca Publica do
+  Projeto LaTeX, distribuido a partir dos arquivos do CTAN no
+  diretorio macros/latex/base/lppl.txt.
+  (C) 2007 Arthur Buchsbaum e Francisco Reinaldo
+
+VERSAO
+  Este eh o turnstile versao 1.0.
+
+MUDANCAS
+  1.0  Primeira versao publica.
+
+Arquivos e Diretorios no CTAN
+  README.pt              Este arquivo.
+  turnstile-pt.dtx       A fonte para o estilo turnstile
+  turnstile-pt.pdf       Versao em pdf do estilo
+  turnstile-pt.ins       Driver para o turnstile-pt.dtx
+  turnstile_artigo.tex   A fonte para o artigo
+  turnstile_artigo.pdf   Versao em pdf da documentacao,
+                         publicada por PracTeX Journal: Numero 2007-3.
+         
+REQUISITOS
+  A instalacao do pacote turnstile requer os pacotes ifthen.
+  Por favor, use <<a derradeira versao do LaTeX>>.
+
+INSTALACAO
+  O procedimento de instalacao eh descrito na documentacao,
+  mas voce pode tambem seguir estes passos:
+
+  1. Puxe os arquivos turnsilte-pt\turnstile-pt.ins e 
+	 turnsilte-pt\turnstile-pt.dtx para um diretorio preferencialmente 
+	 vazio. Se voce pretende manter a documentacao, eh melhor criar 
+	 um diretorio adequado e colocar la todos os arquivos agora mesmo.
+  2. Inicie uma shell onde voce pode entrar com os comandos pelo
+     teclado.
+  3. Va para o diretorio onde voce colocou os arquivos
+     turnstile-pt.ins e turnstile-pt.dtx.
+  4. Execute o comando:
+      pdflatex turnstile-pt.ins
+     Voce obtera o arquivo turnstile.sty 
+  5. Execute o comando:
+      pdflatex turnstile-pt.dtx
+     para produzir a documentacao e testar a instalacao.
+     Execute este comando mais uma vez para obter as referencias, antes
+     de consulta-la.
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile-en.pdf b/Master/texmf-dist/doc/latex/turnstile/turnstile-en.pdf
new file mode 100644
index 00000000000..f5c36d573c3
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile-en.pdf
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile-pt.pdf b/Master/texmf-dist/doc/latex/turnstile/turnstile-pt.pdf
new file mode 100644
index 00000000000..a49ca8f76ac
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile-pt.pdf
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile_article.pdf b/Master/texmf-dist/doc/latex/turnstile/turnstile_article.pdf
new file mode 100644
index 00000000000..3a49c5f391a
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile_article.pdf
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile_article.tex b/Master/texmf-dist/doc/latex/turnstile/turnstile_article.tex
new file mode 100644
index 00000000000..90506e8aaa1
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile_article.tex
@@ -0,0 +1,258 @@
+\documentclass{pracjourn}
+                  
+%\usepackage{amsmath}
+\usepackage{turnstile}
+
+\TPJrevision{2007}{08}{18}
+\TPJissue{2007}{3}
+
+\title{A Tool for Logicians}
+
+\author{Arthur Buchsbaum and Francisco Reinaldo}
+\email{arthur@inf.ufsc.br, reinaldo.opus@gmail.com}
+
+\abstract{\textsf{turnstile} is a \LaTeX{} package that allows typesetting of the mathematical logic symbol, ``turnstile'', in all of the various ways it is used. This package was developed because there was no easy way in \LaTeX{} to typeset this symbol in its various forms, and place expressions above and below the crossbar.}
+
+\bibliographystyle{plain}
+
+\begin{document}
+
+\maketitle
+
+\section{Introduction}
+
+Logic is a science whose initial motivation was the analysis of correct reasoning. In recent years it has advanced beyond of the study of reasoning, and has many intersections with research areas such as Mathematics, Philosophy, Computer Science, Linguistics, Physics and Artificial Intelligence. One of the main signs used in Logic is the~turnstile sign, from which there are versions such as ``$\,\vdash$'' and ``$\,\models$'', issued respectively by the \LaTeX\ commands \begin{verb}=\vdash=\end{verb} and \begin{verb}=\models=\end{verb}
+
+\section{The turnstile Project} % (fold)
+\label{sec:turnstile_project}
+
+The turnstile\footnote{\url{http://tug.ctan.org/tex-archive/macros/latex/contrib/turnstile}} is a sign often used by logicians for denoting a consequence relation, related to a given logic, between a collection of formulas and a formula. Many logicians have complained that there is no easy method in \LaTeX\ to typeset turnstile signs.  They occur in many forms, and must be able to have expressions placed correctly above and below them. \LaTeX\ commands such as \begin{verb}=\vdash=\end{verb} and \begin{verb}=\models=\end{verb} typeset the turnstile sign, but they are not capable of placing data below or above them in an acceptable way. For example, sometimes it is necessary to place the name of a considered logical system below the turnstile sign, and sometimes it is necessary to put additional information above it.
+
+\vspace{0.2em}
+
+If we want to say that a formula $P$ is a logical consequence of a collection $\Gamma$ of~formulas in a logic $\mathrm{L}$, we could try to typeset it by \begin{verbatim}\Gamma \vdash_\mathrm{L} P,\end{verbatim} giving $\Gamma \vdash_\mathrm{L} P$.
+
+\medskip
+
+Note that ``$\mathrm{L}$'' was not placed correctly with respect to the turnstile sign; it~should be placed and centred exactly below the sign. With \texttt{turnstile.sty} we can typeset it by \begin{verbatim}\Gamma \sststile{\mathrm{L}}{} P,\end{verbatim} giving $\Gamma \sststile{\mathrm{L}}{} P$.
+
+\medskip
+
+On the other hand, if we want to say that a formula $P$ is a logical semantical consequence of a collection $\Gamma$ of formulas in a logic $\mathrm{L}$, through varying of $x$ and~$y$\footnote{In \cite{BuchsbaumBeziau2004} and \cite{BuchsbaumPequeno1997} varying objects are presented.}, we could try to typeset it by \begin{verbatim}\Gamma \models_\mathrm{L}^{x,y} P,\end{verbatim} giving $\Gamma \models_\mathrm{L}^{x,y} P$.
+
+\medskip
+
+Note that both ``$\mathrm{L}$'' and ``$x,y$'' were not placed correctly with respect to turnstile sign; they should be placed and centered exactly below and above the sign. With \texttt{turnstile.sty} we can typeset it by \begin{verbatim}\Gamma \sdtstile{\mathrm{L}}{x,y} P,\end{verbatim} giving $\Gamma \sdtstile{\mathrm{L}}{x,y} P$.
+
+\medskip
+
+%%% LAC: Rei - it will take a super-logician to figure out the following paragraphs ;-)
+
+The commands provided by this style are all formed by the string ``tstile'' preceded by a string with two or three letters. These letters indicate the kind of~lines to be drawn successively; they can be ``n'', ``s'', ``d'', or ``t''. The~letter~``n'' says that the line is empty, the letter ``s'' that the line is single, the letter ``d'' that the line is double, and finally ``t'' indicates that the line is triple. The corresponding commands for the two-lettered strings provide the most common turnstile signs, in which there is not a second vertical line following the~horizontal line. The first letter of these strings indicates the kind of the vertical line and the second the kind of the horizontal line to be drawn after the vertical line. The three-lettered strings can contain any of the letters ``n'', ``s'', ``d'', and~``t'', with~the restriction that the last letter must not be ``n'', because the~case in which the third line is empty is already dealt with by the commands with two-lettered strings preceding ``tstile''. The first letter specifies the kind of the first vertical line, the~second the kind of the horizontal line, and the third letter the kind of the second vertical line.
+
+All these commands have three arguments, and the first one is optional.
+
+The first argument, which is optional, gives the size by which the internal expressions must be displayed: ``d'' for displayed formulas, ``t'' for text formulas, ``s'' for first subscript or superscript formulas, and ``ss'' for later subscript or superscript formulas. The default value is ``s''. The result of applying ``t'' or ``d'' is the same, except if there is a mathematical sign in the second or third argument issued in~distinct ways, depending on whether it is used in text math mode or displayed math mode.
+
+The second and third arguments provide the expressions to be placed below and above the turnstile sign respectively, where both these expressions are converted to the size specified by the first argument. On the other hand, if the~second or the third argument is empty, then nothing is put below or above the turnstile sign.
+
+\section{Examples} % (fold)
+\label{sec:examples}
+
+Some examples are shown below.  For the sake of illustration, $\Gamma$ is a~given collection of formulas and $P$ is a logical formula. Of course, the signs ``$\Gamma$'' and ``$P$'' illustrate only one possible context in which the turnstile sign could appear.
+
+\begin{verbatim}
+\Gamma \sststile{}{} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{}{} P \end{equation} \vspace{0.4em}
+
+\pagebreak
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPD}}{} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPD}}{} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{}{x,y} P\end{equation} \vspace{0.4em}
+
+If the optional argument is not used, then the result is the same as if ``s'' was the optional argument:
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+          
+\pagebreak
+
+\begin{verbatim}
+\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+     
+\pagebreak
+
+\begin{verbatim}
+\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+         
+\begin{verbatim}
+\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \nsdtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}  \nsdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+ 
+\pagebreak
+
+\begin{verbatim}
+\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+
+\begin{verbatim}
+\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+Below are some examples of mathematical expressions below and~above the turnstile sign which show how it changes depending on the optional argument. If no optional argument is given, then it is considered to be ``s''.
+
+The reader should also note that the vertical lines don't stretch according to~the~heights of the expressions located below and above the turnstile sign.  Because logicians use this sign mainly in text mode, we feel that it should have a standard height.
+
+\begin{verbatim}
+\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\section{Conclusions} % (fold)
+\label{sec:conclusions}
+
+The package \texttt{turnstile.sty} seems to be adequate for typesetting the turnstile sign in~its many forms.  It correctly places additional expressions below and above it, if necessary, and stretches the the crossbar width as much as needed to contain the expressions.
+
+For a future version of this package, we want to look at changing the height of the turnstile sign.  This will take into account the heights of the~expressions above and below, similar to the way we currently allow for the widths of the expressions.
+
+\begin{thebibliography}{1}
+
+\bibitem{BuchsbaumBeziau2004}
+Arthur Buchsbaum and Jean-Yves B{\'e}ziau.
+\newblock Introduction of implication and~generalization in axiomatic calculi.
+\newblock In Jean-Yves B{\'e}ziau, Alexandre~Costa Leite, and Alberto Facchini,
+  editors, {\em Aspects of Universal Logic}, number~17 in~Travaux de Logique,
+  page 231. Centre de Recherches S{\'e}miologiques, \mbox{Universit{\'e}} de
+  Neuch{\^a}tel, December 2004.
+
+\bibitem{BuchsbaumPequeno1997}
+Arthur Buchsbaum and Tarcisio Pequeno.
+\newblock A general treatment for the deduction theorem in open calculi.
+\newblock {\em Logique et Analyse}, 157:9--29, January--March 1997.
+
+\bibitem{KopkaDaly1999}
+Helmut Kopka and Patrick~W. Daly.
+\newblock {\em A Guide to \LaTeX}.
+\newblock Addison-Wesley, 1999.
+
+\bibitem{Lamport1994}
+Leslie Lamport.
+\newblock {\em \LaTeX\ -- A Document Preparation System -- User's Guide and Reference Manual}.
+\newblock Addison-Wesley, 1994.
+
+\bibitem{NerodeShore1997}
+Anil Nerode and Richard~A. Shore.
+\newblock {\em Logic for Applications}.
+\newblock Springer, 1997.
+
+\bibitem{Nolt1996}
+John Nolt.
+\newblock {\em Logics}.
+\newblock Wadsworth, 1996.
+
+\end{thebibliography}
+
+\end{document}
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.pdf b/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.pdf
new file mode 100644
index 00000000000..b843213632e
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.pdf
diff --git a/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.tex b/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.tex
new file mode 100644
index 00000000000..749cb098d35
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/turnstile/turnstile_artigo.tex
@@ -0,0 +1,274 @@
+% -*- TeX -*- BR -*-
+
+\documentclass[portuguese]{pracjourn}
+
+\usepackage{turnstile}
+%\usepackage{english}
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+
+\TPJrevision{2007}{08}{18}
+\TPJissue{2007}{3}
+
+%%% Changing the name of the info labels:
+\renewcommand\abstractname{Resumo}
+\renewcommand\emailname{Contacto}
+\renewcommand\websitename{S\'itio}
+%%%
+
+\title{Uma Ferramenta para Lógicos}
+\author{Arthur Buchsbaum e Francisco Reinaldo}
+\email{arthur@inf.ufsc.br, reinaldo.opus@gmail.com}  
+\website{http://www.inf.ufsc.br/~arthur}
+
+\abstract{\textsf{turnstile} é um estilo baseado em \texttt{article.cls}, usado para composição de artigos. Entre outros usos, a barra de Frege é usada pelos lógicos para denotar a relação de conseqüência, com respeito a uma dada lógica, entre coleções de fórmulas e fórmulas. Pesquisadores em Lógica têm sentido falta de uma rotina em \LaTeX\ para obter a barra de Frege, em alguma das diversas formas em que esta é utilizada.}
+
+\bibliographystyle{plain}
+
+\begin{document}
+
+\maketitle
+
+\section{Introdução}
+
+A Lógica é uma ciência cuja motivação inicial foi a análise do raciocínio correto. Hoje em dia ela está muito além do estudo do raciocínio, ela tem muitas ligações com áreas de pesquisa tais como Matemática, Filosofia, Informática, Lingüística, Física e Inteligência Artificial. Um dos sinais de maior utilização na Lógica é a barra de Frege\footnote{Gottlob Frege (1848--1925) é considerado por muitos o pai da lógica quantificacional e da moderna filosofia da linguagem, e adotou em sua obra o símbolo que é o tema deste artigo. Maiores detalhes estão em \cite{Frege1978}.}, da qual existem versões tais como ``$\,\vdash$'' e~``$\,\models$'', obtidas respectivamente pelos comandos de \LaTeX\ \begin{verb}=\vdash=\end{verb} e \begin{verb}=\models=\end{verb}.
+
+\section{O Projeto turnstile}
+\label{sec:turnstile_project}
+
+A barra de Frege\footnote{\url{http://tug.ctan.org/tex-archive/macros/latex/contrib/turnstile}} é um sinal muito utilizado pelos lógicos para denotar a relação de conseqüência, em uma dada lógica, entre coleções de fórmulas e fórmulas. A existência de uma rotina em \LaTeX\ que desenhe adequadamente este símbolo tem feito falta, na composição de artigos que utilizam este sinal, em diversas das formas em que este aparece, incluindo a colocação de dados nas posições corretas acima e abaixo deste sinal. Comandos de \LaTeX\ tais como \begin{verb}=\vdash=\end{verb} e~\begin{verb}=\models=\end{verb}, embora resultem em versões da barra de Frege, não são capazes de colocar nos lugares adequados eventuais dados acima ou abaixo da mesma. Por exemplo, algumas vezes é necessário colocar abaixo da barra de Frege o nome de um determinado sistema lógico, e algumas vezes é preciso colocar acima desta alguma informação adicional.
+
+\vspace{0.2em}
+
+Se queremos dizer que uma fórmula $P$ é conseqüência lógica de uma coleção $\Gamma$ de fórmulas em uma lógica $\mathrm{L}$, poderíamos tentar obter isto por \begin{verbatim}\Gamma \vdash_\mathrm{L} P,\end{verbatim} obtendo $\Gamma \vdash_\mathrm{L} P$.
+
+\medskip
+
+Note que ``$\mathrm{L}$'' não foi bem posicionado com respeito à barra de Frege, ``$\mathrm{L}$'' deveria ser colocado bem abaixo e centralizado. Com \texttt{turnstile.sty} podemos obter isto por \begin{verbatim}\Gamma \sststile{\mathrm{L}}{} P,\end{verbatim} resultando em $\Gamma \sststile{\mathrm{L}}{} P$.
+
+\medskip
+
+Além disto, se quisermos dizer que uma fórmula $P$ é conseqüência lógica de uma coleção $\Gamma$ de fórmulas em uma lógica $\mathrm{L}$, pela variação de $x$ e $y$\footnote{Em \cite{BuchsbaumBeziau2004,BuchsbaumPequeno1997,BuchsbaumPequeno1998} objetos variantes são apresentados.}, poderíamos tentar obter isto por \begin{verbatim}\Gamma \models_\mathrm{L}^{x,y} P,\end{verbatim} resultando em $\Gamma \models_\mathrm{L}^{x,y} P$.
+
+\medskip
+
+Também neste caso, ``$\mathrm{L}$'' e ``$x,y$'' não foram posicionados corretamente com respeito à barra de Frege, estas expressões deveriam ser centralizadas e colocadas, respectivamente, logo abaixo e logo acima deste sinal. Com \texttt{turnstile.sty} podemos obter isto por \begin{verbatim}\Gamma \sdtstile{\mathrm{L}}{x,y} P,\end{verbatim} resultando em $\Gamma \sdtstile{\mathrm{L}}{x,y} P$.
+
+\medskip
+
+Os comandos deste estilo são formados pela samblagem ``tstile'', precedida por uma samblagem com duas ou três letras. Estas letras indicam o tipo das linhas a serem desenhadas sucessivamente; elas podem ser ``n'', ``s'', ``d'' ou ``t''. A letra ``n'' informa que a linha correspondente é vazia, a letra ``s'' que a linha é simples, a letra ``d'' que é dupla, e finalmente a letra ``t'' que é tripla. Os comandos correspondentes às samblagens de duas letras resultam nas barras de Frege mais utilizadas, nas quais não é desenhada uma segunda linha vertical seguindo a linha horizontal. A primeira letra destas samblagens indica o tipo da linha vertical, enquanto que a segunda o tipo da linha horizontal a ser desenhada após a linha vertical. As samblagens de três letras podem conter qualquer uma das letras ``n'', ``s'', ``d'' ou ``t'', com a restrição de que a derradeira letra seja distinta de ``n'', porque o caso no qual a terceira linha é vazia já foi tratado pelos comandos com samblagens de duas letras precedendo ``tstile''. A primeira letra informa o tipo da primeira linha vertical, a segunda o tipo da linha horizontal e, finalmente, a terceira o tipo da segunda linha vertical.
+
+Estes comandos possuem três argumentos, onde o primeiro é opcional.
+
+O primeiro argumento é opcional, este informa o tamanho em que as expressões internas na barra de Frege devem ser exibidas, ``d'' para expressões (normalmente) em linhas exclusivas, ``t'' para expressões (normalmente) inseridas no texto corrente, ``s'' para expressões subscritas ou sobrescritas, e ``ss'' para expressões ainda menores, subscritas ou sobrescritas com respeito às do tipo anterior. O valor predeterminado é ``s''. O resultado de aplicar ``d'' ou ``t'' é o mesmo, a não ser que haja um sinal matemático no segundo ou terceiro argumento exibido de formas distintas, dependendo se este está em expressões (normalmente) de linhas exclusivas, ou em expressões (normalmente) inseridas no texto corrente.
+
+O segundo e o terceiro argumento fornecem as expressões a serem colocadas abaixo e acima da barra de Frege, onde ambas são convertidas para o tamanho especificado no primeiro argumento. Por outro lado, se o segundo ou o terceiro argumento foram vazios, então nada é colocado abaixo ou acima deste sinal.
+
+\section{Exemplos}
+\label{sec:examples}
+
+Damos a seguir alguns exemplos, onde, à guisa de ilustração, $\Gamma$ é uma coleção de fórmulas e $P$ é uma fórmula de uma lógica. Naturalmente, os sinais ``$\Gamma$'' e ``$P$'' apenas servem para dar um possível contexto no qual a barra de Frege pode aparecer, entre outros.
+
+\begin{verbatim}
+\Gamma \sststile{}{} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{}{} P \end{equation}\vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPD}}{} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPD}}{} P\end{equation}\vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{}{x,y} P\end{equation} \vspace{0.4em}
+
+Se o argumento opcional não é usado, então o resultado é o mesmo no qual ``s'' é o argumento opcional:
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P\end{equation}\vspace{0.4em}
+\enlargethispage{-2\baselineskip}
+
+\begin{verbatim}
+\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+
+\begin{verbatim}
+\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+     
+\pagebreak
+
+\begin{verbatim}
+\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \nsdtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}  \nsdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+     
+\pagebreak
+
+\begin{verbatim}
+\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P
+\end{verbatim}
+\begin{equation}\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
+
+São dados a seguir alguns exemplos de expressões matemáticas abaixo e acima da barra de Frege que mudam bastante, dependendo do argumento opcional. Se nenhum argumento opcional for dado, então este é considerado ``s''.
+
+O leitor pode observar que as linhas verticais não crescem de acordo com a altura das expressões localizadas abaixo e acima da barra de Frege, isto porque consideramos que este sinal deve ter uma altura padrão, pois entendemos que este símbolo aparece principalmente inserido no texto corrente.
+          
+\pagebreak
+
+\begin{verbatim}
+\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\begin{verbatim}
+\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P
+\end{verbatim}
+\begin{equation}\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}
+
+\section{Conclusões}
+\label{sec:conclusions}
+
+O estilo \texttt{turnstile.sty} parece ser adequado para a obtenção da barra de Frege, em muitas das formas em que esta aparece, e coloca corretamente expressões adicionais abaixo e acima desta, se necessário, bem como a largura deste sinal cresce tanto quanto for preciso, quando uma ou ambas as expressões são largas.
+
+Para uma versão futura deste pacote, pretendemos examinar a conveniência de mudar também a altura da barra de Frege, levando assim em conta as alturas das expressões eventualmente colocadas abaixo ou acima deste sinal, além das suas larguras, como já procedemos.
+
+\begin{thebibliography}{1}
+
+\bibitem{BuchsbaumBeziau2004}
+Arthur Buchsbaum e Jean-Yves Béziau.
+\newblock Introduction of implication and generalization in axiomatic calculi.
+\newblock Em Jean-Yves Béziau, Alexandre~Costa Leite, e Alberto Facchini,
+  editores, {\em Aspects of Universal Logic}, número 17 em Travaux de Logique,
+  página 231. Centre de Recherches Sémiologiques, Université de Neuchâtel, Dezembro de 2004.
+
+\bibitem{BuchsbaumPequeno1997}
+Arthur Buchsbaum e Tarcisio Pequeno.
+\newblock A general treatment for the deduction theorem in open calculi.
+\newblock {\em Logique et Analyse}, 157:9--29, janeiro--março de 1997.
+
+\bibitem{BuchsbaumPequeno1998}
+Arthur Buchsbaum e Tarcisio Pequeno.
+\newblock A introdução da implicação em cálculos axiomáticos abertos.
+\newblock Em {\em Anais do IV Encontro de Filosofia Analítica}, páginas~61--75, 1998.
+
+\bibitem{Frege1978}
+Gottlob Frege.
+\newblock {\em Lógica e Filosofia da Linguagem}.
+\newblock Editora Cultrix e Editora da Universidade de São Paulo, 1978.
+
+\bibitem{KopkaDaly1999}
+Helmut Kopka and Patrick~W. Daly.
+\newblock {\em A Guide to \LaTeX}.
+\newblock Addison-Wesley, 1999.
+
+\bibitem{Lamport1994}
+Leslie Lamport.
+\newblock {\em \LaTeX\ -- A Document Preparation System -- User's Guide and Reference Manual}.
+\newblock Addison-Wesley, 1994.
+
+\bibitem{NerodeShore1997}
+Anil Nerode and Richard~A. Shore.
+\newblock {\em Logic for Applications}.
+\newblock Springer, 1997.
+
+\bibitem{Nolt1996}
+John Nolt.
+\newblock {\em Logics}.
+\newblock Wadsworth, 1996.
+
+\end{thebibliography}
+
+\end{document}