logicproof (21mar14)

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

8 files changed, 881 insertions, 2 deletions

diff --git a/Master/texmf-dist/doc/latex/logicproof/README b/Master/texmf-dist/doc/latex/logicproof/README
new file mode 100644
index 00000000000..1713e38bafa
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/logicproof/README
@@ -0,0 +1,13 @@
+The `logicproof' package
+
+This package provides environments for creating Fitch-style box proofs for
+propositional and predicate logic. In this style, each line of the proof
+contains a statement and a justification, and subproofs within the larger
+proof are enclosed in a box. For an example of this proof style, see the manual
+in logicproof.pdf.
+
+This code is released under the LaTeX Project Public License.
+
+History:
+2014/03/20 - First version intended for public consumption
+2004/12/05 - Initial version created for personal use at school
diff --git a/Master/texmf-dist/doc/latex/logicproof/logicproof.pdf b/Master/texmf-dist/doc/latex/logicproof/logicproof.pdf
new file mode 100644
index 00000000000..06d7c837872
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/logicproof/logicproof.pdf
diff --git a/Master/texmf-dist/source/latex/logicproof/logicproof.dtx b/Master/texmf-dist/source/latex/logicproof/logicproof.dtx
new file mode 100644
index 00000000000..6e1a3ea7ccf
--- /dev/null
+++ b/Master/texmf-dist/source/latex/logicproof/logicproof.dtx
@@ -0,0 +1,638 @@
+% \iffalse meta-comment
+%
+% Copyright (C) 2014 by Alan Davidson <alan.davidson@gmail.com>
+% ---------------------------------------------------------------------------
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+%   http://www.latex-project.org/lppl.txt
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Alan Davidson.
+%
+% This work consists of the files logicproof.dtx and logicproof.ins
+% and the derived filebase logicproof.sty.
+%
+% \fi
+%
+% \iffalse
+%<*driver>
+\ProvidesFile{logicproof.dtx}
+%</driver>
+%<package>\NeedsTeXFormat{LaTeX2e}
+%<package>\ProvidesPackage{logicproof}[2014/03/20 v1.0 Box proofs for propositional logic]
+%
+%<*driver>
+\documentclass{ltxdoc}
+\usepackage{logicproof}[2014/03/20]
+\EnableCrossrefs
+\CodelineIndex
+\RecordChanges
+\begin{document}
+  \DocInput{logicproof.dtx}
+  \PrintChanges
+  \PrintIndex
+\end{document}
+%</driver>
+% \fi
+%
+% \CheckSum{0}
+%
+% \CharacterTable
+%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%   Digits        \0\1\2\3\4\5\6\7\8\9
+%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%   Dollar        \$     Percent       \%     Ampersand     \&
+%   Acute accent  \'     Left paren    \(     Right paren   \)
+%   Asterisk      \*     Plus          \+     Comma         \,
+%   Minus         \-     Point         \.     Solidus       \/
+%   Colon         \:     Semicolon     \;     Less than     \<
+%   Equals        \=     Greater than  \>     Question mark \?
+%   Commercial at \@     Left bracket  \[     Backslash     \\
+%   Right bracket \]     Circumflex    \^     Underscore    \_
+%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%   Right brace   \}     Tilde         \~}
+%
+%
+% \changes{1.0}{2014/03/20}{First version for public release}
+% \changes{0.1}{2004/12/05}{Initial version created}
+% \GetFileInfo{logicproof.dtx}
+%
+% \DoNotIndex{\newcommand,\newenvironment}
+%
+% \providecommand*{\url}{\texttt}
+% \title{The \textsf{logicproof} package}
+% \author{Alan Davidson \\ \url{alan.davidson@gmail.com}}
+% \date{20 March 2014}
+%
+% \maketitle
+%
+% \section{Introduction}
+%
+% This package provides support for Fitch-style box proofs, intended to be used
+% for proofs in propositional logic and predicate logic. In this proof style,
+% each statement of the proof is accompanied by a justification, and subproofs
+% or lemmata within a larger proof are enclosed in boxes to separate them from
+% the rest of the proof.
+%
+% \section{Usage}
+%
+% \DescribeEnv{logicproof}
+% The |logicproof| environment takes a single argument, which should be a
+% nonnegative integer describing the maximum number of nested subproofs that
+% this proof will contain. Each line of the proof consists of two main
+% columns: the proof statement of the current line, followed by an ampersand
+% (|&|), followed by the justification for the statement.
+% Lines should be separated from each other by a |\\|.
+% The column of proof statements defaults to
+% math mode, while the justification column defaults to normal text.
+%
+% If you add a |\label| within a proof, the corresponding |\ref| will be the
+% current line number.
+%
+% \DescribeEnv{subproof}
+% Within these logic proofs, it is often necessary to make subproofs which begin
+% by making some sort of assumption that does not necessarily hold in the
+% broader proof. To delineate the scope of these assumptions, use the |subproof|
+% environment, which will draw a box around the statements of the proof for
+% which these assumptions should hold. Subproofs can be nested within each
+% other, up to the maximum level provided as an argument to the |logicproof|
+% environment.
+%
+% Within a subproof, the format of each line is exactly the same as in the
+% |logicproof| environment: a proof statement, followed by an ampersand (|&|),
+% followed by a justification for the statement, with |\\| at the end of every
+% line except the last one (which instead ends with |\end{subproof}|).
+%
+% If a statement has an empty justification, it is still important to put in the
+% |&| to separate out the column in which the justification would go, or else
+% the right sides of the subproof boxes will be misaligned for this statement.
+%
+% The previous line before a subproof begins should end in either |\\| or
+% |\end{subproof}|.
+%
+% A warning for advanced \LaTeX~users: although most environments make their own
+% groups (such that changes made within an environment go out of scope at the
+% end of it), the |subproof| environment does not! Any changes made within a
+% |subproof|
+% environment will not go out of scope until the enclosing |logicproof|
+% environment ends. This was done because groups cannot cross alignment tabs,
+% but the |subproof| environment needs to use the same alignment as the
+% enclosing |logicproof| environment does (or else they won't line up together).
+% An inconvenient side effect of this is that when you forget to put in a
+% |\end{subproof}|, the error message about mismatched environments points to
+% the line number where the enclosing |logicproof| environment started, rather
+% than the offending |subproof| environment.
+%
+% \section{Example}
+%
+% This example proves the validity of the sequent
+% $(p\lor q)\lor r\vdash p\lor (q\lor r)$. There are many different styles that
+% can be used for the justification of each step; we are using the style found
+% in \emph{Logic in Computer Science: Modelling and Reasoning about Systems} by
+% Huth and Ryan.
+%
+%\begin{verbatim}
+%\begin{logicproof}{2}
+%  (p\lor q)\lor r & premise\\
+%  \begin{subproof}
+%    (p\lor q) & assumption\\
+%    \begin{subproof}
+%      p & assumption\\
+%      p\lor (q\lor r) & $\lor\mathrm{i}_1$, 3
+%    \end{subproof}
+%    \begin{subproof}
+%      q & assumption\\
+%      q\lor r & $\lor\mathrm{i}_1$, 5\\
+%      p\lor (q\lor r) & $\lor\mathrm{i}_2$, 6
+%    \end{subproof}
+%    p\lor (q\lor r) & $\lor$e, 2, 3--4, 5--7
+%  \end{subproof}
+%  \begin{subproof}
+%    r & assumption\\
+%    q\lor r & $\lor\mathrm{i}_2$, 9\\
+%    p\lor (q\lor r) & $\lor\mathrm{i}_2$, 10
+%  \end{subproof}
+%  p\lor (q\lor r) & $\lor$e, 1, 2--8, 9--11
+%\end{logicproof}
+%\end{verbatim}
+% This compiles into the following:
+%\begin{logicproof}{2}
+%  (p\lor q)\lor r & premise\\
+%  \begin{subproof}
+%    (p\lor q) & assumption\\
+%    \begin{subproof}
+%      p & assumption\\
+%      p\lor (q\lor r) & $\lor\mathrm{i}_1$, 3
+%    \end{subproof}
+%    \begin{subproof}
+%      q & assumption\\
+%      q\lor r & $\lor\mathrm{i}_1$, 5\\
+%      p\lor (q\lor r) & $\lor\mathrm{i}_2$, 6
+%    \end{subproof}
+%    p\lor (q\lor r) & $\lor$e, 2, 3--4, 5--7
+%  \end{subproof}
+%  \begin{subproof}
+%    r & assumption\\
+%    q\lor r & $\lor\mathrm{i}_2$, 9\\
+%    p\lor (q\lor r) & $\lor\mathrm{i}_2$, 10
+%  \end{subproof}
+%  p\lor (q\lor r) & $\lor$e, 1, 2--8, 9--11
+%\end{logicproof}
+%
+% \section{Advanced Configuration}
+%
+% There are two lengths that can be configured manually if desired. 
+%
+% \DescribeMacro{\subproofhorizspace}
+% The
+% horizontal distance between the sides of nested boxes is the length stored in 
+% |\subproofhorizspace|. If you have many nested subproofs, it might be
+% desirable to make this space larger so that it is easier to distinguish
+% between them.
+%
+% \DescribeMacro{\intersubproofvertspace}
+% An extra vertical space of length
+% |\intersubproofvertspace| is added after each statement in the proof. The
+% intention here is to have this much space between consecutive subproofs. This
+% is to say, when one subproof ends
+% and the next subproof begins immediately, this is the distance between the
+% bottom edge of the ending subproof and the top edge of the beginning subproof.
+% This space is inserted after each line, however, so that the vertical spacing
+% between them is consistent regardless of whether subproofs are begun or ended.
+% If you want more compact proofs and you never use consecutive
+% subproofs, it might be useful to reduce or remove this extra space.
+%
+% \section{Constraints}
+% The environments in this package might not work properly if any of the
+% following constraints are violated. These should not be difficult burdens;
+% they are listed here mainly for completeness.
+% \begin{itemize}
+% \item Each proof and each subproof must be at least 1 statement long.
+% \item Each subproof must start with at least 1 statement before containing
+% another subproof inside itself. You should not have a subproof that
+% immediately begins with a nested subproof.
+% \item The end of each subproof must have at least 1 statement (or
+% a new subproof) following
+% it; a single proof statement cannot end multiple subproofs at once.
+% Consequently, the last
+% statement of the top-level proof must be outside of all subproofs. It is okay
+% to immediately start a new subproof after ending a previous subproof.
+% \end{itemize}
+%
+% \StopEventually{\PrintIndex\PrintChanges}
+%
+% \section{Summary of Implementation}
+%
+% The |logicproof| environment is built on the |tabular| environment. It has a
+% column for the line number, a column for each possible nested subproof, a
+% column for the statement, a column for the justification, and then a second
+% column for each possible nested subproof.
+% The columns corresponding to nested subproofs either contain a |\vline| if the
+% subproof is currently being used, or nothing if the subproof is not being
+% used.
+% When a subproof is begun or ended, a |\cline| is used to draw
+% horizontal lines between the columns corresponding to that subproof. In order
+% to prevent multiple |\cline|'s from overlapping when one subproof is ended and
+% another is immediately begun, each statement in the proof actually ends with
+% a negative vertical space backing up to the previous line, then a space down
+% |\intersubproofvertspace| and a redrawing of the subproof lines again to cover
+% the extra space.
+%
+% \section{Implementation}
+%
+% \iffalse
+%<*package>
+% \fi
+%
+%    \begin{macrocode}
+\RequirePackage{array}
+\RequirePackage{ifthen}
+%    \end{macrocode}
+%    \begin{macro}{\subproofhorizspace}
+%    \begin{macro}{\intersubproofvertspace}
+% We allow the user to configure the horizontal and vertical distance between
+% the edges of the boxes.
+%    \begin{macrocode}
+\newlength{\subproofhorizspace}
+\setlength{\subproofhorizspace}{0.5em}
+\newlength{\intersubproofvertspace}
+\setlength{\intersubproofvertspace}{0.333em}
+%    \end{macrocode}
+%    \end{macro}
+%    \end{macro}
+% We use a variety of counters to keep track of the state.
+%    \begin{macrocode}
+\newcounter{lp@line}% Current line number on the proof
+\newcounter{lp@nested}% Number of nested subproofs we're currently in
+\newcounter{lp@total@nests}% Maximum number of nested subproofs allowed
+\newcounter{lp@cline@1}% Used to draw horizontal lines in subproofs
+\newcounter{lp@cline@2}% Also used to draw horizontal lines in subproofs
+\newcounter{lp@temp}% Temporary storage counter
+%    \end{macrocode}
+%
+% \begin{environment}{logicproof}
+% Use this to make a logic proof. The argument it takes is the
+% maximum number of nested subproofs you will use. 
+%    \begin{macrocode}
+\newenvironment{logicproof}[1]{%
+  \setcounter{lp@line}{0}%
+  \setcounter{lp@nested}{0}%
+  \setcounter{lp@total@nests}{#1}%
+  \setlength{\tabcolsep}{0mm}%
+%    \end{macrocode}
+% When using the array package, the tabular environment contains the statement
+% |\let\\\@arraycr| (note that with the array package, |\@tabularcr| is replaced
+% with |\@arraycr| even within the tabular environment). So, to modify the
+% behavior of |\\|, we're actually going to modify |\@arraycr|. Save a copy of the
+% original definition first, so that we can use it inside our new definition.
+% Remember that when the logicproof environment finishes, this redefinition
+% will go out of scope and revert to the previous version, so we won't ruin
+% any future uses of the tabular environment.
+%    \begin{macrocode}
+  \let\lp@orig@arraycr\@arraycr%
+  \renewcommand{\@arraycr}{\lp@cr}%
+%    \end{macrocode}
+% Get labels to work in proofs by defining |\@currentlabel| to always be the
+% line number, regardless of where we are in the proof. Note that the usual
+% approach of using
+% |\refstepcounter{lp@line}| doesn't work because it goes out of scope by the
+% time we get to the next cell in the tabular environment.
+%    \begin{macrocode}
+  \renewcommand{\@currentlabel}{\p@lp@line\thelp@line}%
+%    \end{macrocode}
+% If the maximum number of nested subproofs is 0, we need a slightly different
+% column format, because the array environment doesn't like it when you repeat a
+% formatting group 0 times.
+%    \begin{macrocode}
+  \ifthenelse{%
+    0=#1%
+  }{%
+    \def\lp@tab@format{{r@{~~~}>{$}l<{$}@{~~~~}l}}%
+  }{%
+%    \end{macrocode}
+% Although we could use the |array| package's |>{...}| and |<{...}| features to
+% have automatic placement of the vertical lines on the sides of subproofs,
+% we would not be able to get the horizontal lines at the tops and bottoms
+% of the subproofs to line up properly. Consequently, we go with the ``old
+% school'' approach of putting subproofs in their own columns, so that we
+% can use |\cline| to put the horizontal lines in their proper places.
+%    \begin{macrocode}
+    \def\lp@tab@format%
+        {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
+  }%
+  \center%
+%    \end{macrocode}
+% We use the |tabular| environment instead of the |array| environment because
+% we want
+% to be able to have labels on individual lines. Since the entirety of the
+% |array| environment is in math mode, it does not support more than one label
+% per array.
+%    \begin{macrocode}
+  \expandafter\tabular\lp@tab@format%
+  \lp@start@proof@line%
+}{%
+  \lp@stop@proof@line%
+  \endtabular%
+  \endcenter%
+%    \end{macrocode}
+% To ensure that no one tries using the subproof environment outside of the
+% logicproof environment, set the maximum number of nested subproofs to 0.
+%    \begin{macrocode}
+  \setcounter{lp@total@nests}{0}%
+%    \end{macrocode}
+% Finally, make sure that all open subproofs have been closed. We do this last
+% because if a subproof is still open, we need to set |\@currenvir| properly
+% for |\end| to check and throw errors on, but previous commands have
+% |\endgroup|'s that make it revert to previous definitions.
+%    \begin{macrocode}
+  \ifthenelse{%
+    0=\value{lp@nested}
+  }{% All is well.
+  }{% There are still open subproofs.
+    \def\@currenvir{subproof}%
+  }
+}
+%    \end{macrocode}
+% \end{environment}
+% \begin{environment}{subproof}
+% This environment puts a box around the lines of the proof within it. It
+% should come right after either a |\\| or a |\end{subproof}|.
+%    \begin{macrocode}
+\newenvironment{subproof}{%
+%    \end{macrocode}
+% Make sure we don't start more nested subproofs than the current logicproof
+% environment can handle.
+%    \begin{macrocode}
+  \ifthenelse{%
+    \value{lp@total@nests}>\value{lp@nested}%
+  }{% All is well; don't do anything.
+  }{%
+    \PackageError{logicproof}{Too many nested subproofs!}{%
+      Increase the maximum number of nested subproofs allowed
+      in the current logicproof environment.%
+    }%
+  }%
+%    \end{macrocode}
+% The |\begin| and |\end| parts of an environment start and end a group, so that
+% macros defined within them have local scope. However, a group cannot cross
+% alignment tabs (|&|'s), which means that this subproof environment, which must
+% cross them, needs to get rid of those extra groups first. So, we immediately
+% end the group that |\begin| created before going on with the subproof. Note
+% that this means any redefinitions of any macros we might have will persist
+% outside this subproof and will not go out of scope until the entire
+% logicproof environment is over. Note also that this approach is slightly
+% brittle: if the implementation of |\begin| and |\end| ever changes, this
+% subproof environment is likely to break.
+%    \begin{macrocode}
+  \endgroup%
+  \lp@stop@proof@line%
+%    \end{macrocode}
+% Ideally, we'd use |\lp@extend@space| here. However, we first need to end the
+% current line, which means putting in |\lp@orig@arraycr| and then going up an
+% extra line in the tabular environment via |\lp@add@space|.
+%    \begin{macrocode}
+  \lp@orig@arraycr%
+  \lp@add@space%
+  \lp@go@up@a@line%
+  \stepcounter{lp@nested}%
+  \lp@cr@clines%
+%    \end{macrocode}
+% The current line number was added in before this subproof was started. Do
+% not add it in again now; just skip over the line number entry and go
+% straight on to the subproof-drawing stuff.
+%    \begin{macrocode}
+  &%
+  \lp@continue@proof@line%
+}{%
+%    \end{macrocode}
+% If we try ending a subproof that has not yet begun, we will run into trouble
+% with |\cline| trying to draw a horizontal line to a column past the end of the
+% tabular environment. This happens before |\end| actually checks whether we're
+% ending the right environment. In order to get a more useful error message,
+% we first check that there is at least 1 open subproof.
+%    \begin{macrocode}
+  \ifthenelse{%
+    0<\value{lp@nested}%
+  }{% All is well; don't do anything.
+  }{%
+    \PackageError{logicproof}{Cannot end a subproof before it begins}{%
+      You must have a \protect\begin{subproof} before you can use %
+      \protect\end{subproof}.%
+    }%
+  }%
+  \lp@stop@proof@line%
+  \lp@cr@clines%
+  \addtocounter{lp@nested}{-1}%
+  \lp@extend@space%
+  \lp@start@proof@line%
+%    \end{macrocode}
+% Now that we're done with the subproof, we need to create a group because
+% |\end| is expecting us to still be in the group that was started in |\begin|. We
+% also must redefine |\@currenvir| within that group, or the error-checking in
+% |\end| will think we've ended the wrong environment (its previous redefinition
+% went out of scope when we ended the group created by |\begin|).
+%    \begin{macrocode}
+  \begingroup%
+  \def\@currenvir{subproof}%
+}
+%    \end{macrocode}
+% \end{environment}
+% \begin{macro}{\lp@cr}
+% This is what the |\\| will be defined as inside the logicproof environment.
+%    \begin{macrocode}
+\newcommand{\lp@cr}{%
+  \lp@stop@proof@line%
+  \lp@orig@arraycr%
+  \lp@extend@space%
+  \lp@start@proof@line%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@go@up@a@line}
+% This moves up one entire line in the proof.
+%    \begin{macrocode}
+\newcommand{\lp@go@up@a@line}{%
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+  \vspace{-\intersubproofvertspace}%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@add@space}
+% Extends the vertical lines at the sides of the proof down slightly, so that
+% the horizontal lines at the end of the previous subproof and the start of the
+% next one don't overlap. This basically inserts a blank row in the proof (no
+% line number, no statement, no justification; just the subproof lines), then
+% backs up part of a line.
+%    \begin{macrocode}
+\newcommand{\lp@add@space}{%
+  \lp@extend@space%
+%    \end{macrocode}
+% The |\@arstrutbox| is a box containing the minimum array height. Remember that
+% the height of the strut is spread between the height above the baseline and
+% the depth below it!
+%    \begin{macrocode}
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+%    \end{macrocode}
+% Uncommenting this would line things up exactly where they started.
+%    \begin{macrocode}
+  %\vspace{-\intersubproofvertspace}%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@extend@space}
+% This extends the vertical lines at the sides of the subproofs down by
+% an extra |\intersubproofvertspace.| This is done so that two subproofs in a
+% row don't have their horizontal lines overlap each other.
+%    \begin{macrocode}
+\newcommand{\lp@extend@space}{%
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+  \vspace{\intersubproofvertspace}%
+%    \end{macrocode}
+% Now, insert a row that has vertical lines for the subproofs but no line
+% number, proof statement, or justification.
+%    \begin{macrocode}
+  &%
+  \lp@continue@proof@line%
+  &%
+  \lp@stop@proof@line%
+  \lp@orig@arraycr%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@amper}
+% You can't have a |&| in a |\whiledo| loop, but this works instead. 
+%    \begin{macrocode}
+\newcommand{\lp@amper}{&}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@start@proof@line}
+% This macro does everything on a proof line before the statement itself: it
+% increments and prints the line number, then calls
+% |\lp@continue@proof@line| to put in the vertical lines of any subproofs we're
+% currently in.
+%    \begin{macrocode}
+\newcommand{\lp@start@proof@line}{%
+%    \end{macrocode}
+% We use |\stepcounter| instead of |\refstepcounter| here because the changes made
+% by |\refstepcounter| to how labels get made would go out of scope by the time
+% we got to the next cell of the tabular environment (i.e., 2 lines from
+% here). Instead, we redefined |\@currentlabel| at the beginning of the
+% environment to always contain the current value of the |lp@line| counter.
+%    \begin{macrocode}
+  \stepcounter{lp@line}%
+  \arabic{lp@line}.%
+  &%
+  \lp@continue@proof@line%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@continue@proof@line}
+% This macro makes the vertical lines of the subproof boxes on the left side of
+% the proof (i.e., the ones that come between the line numbers and the proof
+% statements). We use |\lp@amper| here because the raw |&| token doesn't play
+% well with |\whiledo| loops.
+%    \begin{macrocode}
+\newcommand{\lp@continue@proof@line}{%
+  \setcounter{lp@temp}{0}%
+  \whiledo{\value{lp@temp}<\value{lp@nested}}{%
+    \vline%
+    \hspace*{\subproofhorizspace}%
+    \lp@amper%
+    \stepcounter{lp@temp}%
+  }%
+  \whiledo{\value{lp@temp}<\value{lp@total@nests}}{%
+    \hspace*{\subproofhorizspace}%
+    \lp@amper%
+    \stepcounter{lp@temp}%
+  }%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@stop@proof@line}
+% This macro makes the vertical lines of the subproof boxes on the right side
+% of the proof (i.e., the ones that come after the justifications for each
+% step). It basically does the same thing as |\lp@continue@proof@line|, but in
+% reverse order. We use |\lp@amper| here because the raw |&| token doesn't play
+% well with |\whiledo| loops.
+%    \begin{macrocode}
+\newcommand{\lp@stop@proof@line}{%
+  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
+    \addtocounter{lp@temp}{-1}%
+    \lp@amper%
+    \hspace*{\subproofhorizspace}%
+  }%
+  \whiledo{\value{lp@temp}>0}{%
+    \addtocounter{lp@temp}{-1}%
+    \lp@amper%
+    \hspace*{\subproofhorizspace}%
+    \vline%
+  }%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@subtract@from@counter}
+% Subtraction by a value in another counter is annoying, but with this we can
+% use |\expandafter| and make it easier.
+%    \begin{macrocode}
+\newcommand{\lp@subtract@from@counter}[2]{%
+  \addtocounter{#2}{-#1}%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@set@clines}
+% This macro sets up where the horizontal bars go for subproofs.
+%    \begin{macrocode}
+\newcommand{\lp@set@clines}{%
+%    \end{macrocode}
+% |lp@cline@1 = lp@nested + 1|
+%    \begin{macrocode}
+  \setcounter{lp@cline@1}{\value{lp@nested}}%
+  \stepcounter{lp@cline@1}% 
+%    \end{macrocode}
+% |lp@cline@2 = 2 * lp@total@nests + 4 - lp@nested|
+%    \begin{macrocode}
+  \setcounter{lp@cline@2}{\value{lp@total@nests}}%
+  \addtocounter{lp@cline@2}{\value{lp@total@nests}}%
+  \addtocounter{lp@cline@2}{4}%
+%    \end{macrocode}
+% Subtracting one counter from another is tricky. We need to expand the value
+% of the counter being subtracted first.
+%    \begin{macrocode}
+  \expandafter\lp@subtract@from@counter\expandafter{%
+      \value{lp@nested}}{lp@cline@2}%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\lp@cr@clines}
+% This macro goes to the next line of the tabular environment and puts in a
+% horizontal line for the beginning or end of the current subproof.
+%    \begin{macrocode}
+\newcommand{\lp@cr@clines}{%
+  \lp@set@clines%
+%    \end{macrocode}
+% We put the |\lp@orig@arraycr| here instead of in |\lp@stop@proof@line| because
+% |\cline| doesn't seem to work properly unless it's right after the carriage
+% return. Even moving it up above |\lp@set@clines| on the previous line messes
+% it up.
+%    \begin{macrocode}
+  \lp@orig@arraycr%
+  \cline{\value{lp@cline@1}-\value{lp@cline@2}}%
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \iffalse
+%</package>
+% \fi
+%
+% \Finale
+\endinput
diff --git a/Master/texmf-dist/source/latex/logicproof/logicproof.ins b/Master/texmf-dist/source/latex/logicproof/logicproof.ins
new file mode 100644
index 00000000000..10c997a8722
--- /dev/null
+++ b/Master/texmf-dist/source/latex/logicproof/logicproof.ins
@@ -0,0 +1,44 @@
+%%
+%% Copyright (C) 2014 by Alan Davidson
+%%
+%% This file may be distributed and/or modified under the
+%% conditions of the LaTeX Project Public License, either
+%% version 1.3 of this license or (at your option) any later
+%% version. The latest version of this license is in:
+%%   http://www.latex-project.org/lppl.txt
+%% and version 1.3 or later is part of all distributions of
+%% LaTeX version 2005/12/01 or later.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/ package }
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2014 by Alan Davidson
+This file may be distributed and/or modified under the
+conditions of the LaTeX Project Public License, either
+version 1.3 of this license or (at your option) any later
+version. The latest version of this license is in:
+http://www.latex-project.org/lppl.txt
+and version 1.3 or later is part of all distributions of
+LaTeX version 2005/12/01 or later.
+\endpreamble
+\generate{\file{logicproof.sty}{\from{logicproof.dtx}{package}}}
+\Msg{*********************************************************}
+\Msg{*}
+\Msg{* To finish the installation you have to move the}
+\Msg{* following file into a directory searched by TeX:}
+\Msg{*}
+\Msg{* \space\space logicproof .sty}
+\Msg{*}
+\Msg{* To produce the documentation run the file package .dtx}
+\Msg{* through LaTeX.}
+\Msg{*}
+\Msg{* Happy TeXing!}
+\Msg{*********************************************************}
+\endbatchfile
diff --git a/Master/texmf-dist/tex/latex/logicproof/logicproof.sty b/Master/texmf-dist/tex/latex/logicproof/logicproof.sty
new file mode 100644
index 00000000000..fa168dba5e0
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/logicproof/logicproof.sty
@@ -0,0 +1,181 @@
+%%
+%% This is file `logicproof.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% logicproof.dtx  (with options: `package')
+%% 
+%% This is a generated file.
+%% 
+%% Copyright (C) 2014 by Alan Davidson
+%% This file may be distributed and/or modified under the
+%% conditions of the LaTeX Project Public License, either
+%% version 1.3 of this license or (at your option) any later
+%% version. The latest version of this license is in:
+%% http://www.latex-project.org/lppl.txt
+%% and version 1.3 or later is part of all distributions of
+%% LaTeX version 2005/12/01 or later.
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{logicproof}[2014/03/20 v1.0 Box proofs for propositional logic]
+\RequirePackage{array}
+\RequirePackage{ifthen}
+\newlength{\subproofhorizspace}
+\setlength{\subproofhorizspace}{0.5em}
+\newlength{\intersubproofvertspace}
+\setlength{\intersubproofvertspace}{0.333em}
+\newcounter{lp@line}% Current line number on the proof
+\newcounter{lp@nested}% Number of nested subproofs we're currently in
+\newcounter{lp@total@nests}% Maximum number of nested subproofs allowed
+\newcounter{lp@cline@1}% Used to draw horizontal lines in subproofs
+\newcounter{lp@cline@2}% Also used to draw horizontal lines in subproofs
+\newcounter{lp@temp}% Temporary storage counter
+\newenvironment{logicproof}[1]{%
+  \setcounter{lp@line}{0}%
+  \setcounter{lp@nested}{0}%
+  \setcounter{lp@total@nests}{#1}%
+  \setlength{\tabcolsep}{0mm}%
+  \let\lp@orig@arraycr\@arraycr%
+  \renewcommand{\@arraycr}{\lp@cr}%
+  \renewcommand{\@currentlabel}{\p@lp@line\thelp@line}%
+  \ifthenelse{%
+    0=#1%
+  }{%
+    \def\lp@tab@format{{r@{~~~}>{$}l<{$}@{~~~~}l}}%
+  }{%
+    \def\lp@tab@format%
+        {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
+  }%
+  \center%
+  \expandafter\tabular\lp@tab@format%
+  \lp@start@proof@line%
+}{%
+  \lp@stop@proof@line%
+  \endtabular%
+  \endcenter%
+  \setcounter{lp@total@nests}{0}%
+  \ifthenelse{%
+    0=\value{lp@nested}
+  }{% All is well.
+  }{% There are still open subproofs.
+    \def\@currenvir{subproof}%
+  }
+}
+\newenvironment{subproof}{%
+  \ifthenelse{%
+    \value{lp@total@nests}>\value{lp@nested}%
+  }{% All is well; don't do anything.
+  }{%
+    \PackageError{logicproof}{Too many nested subproofs!}{%
+      Increase the maximum number of nested subproofs allowed
+      in the current logicproof environment.%
+    }%
+  }%
+  \endgroup%
+  \lp@stop@proof@line%
+  \lp@orig@arraycr%
+  \lp@add@space%
+  \lp@go@up@a@line%
+  \stepcounter{lp@nested}%
+  \lp@cr@clines%
+  &%
+  \lp@continue@proof@line%
+}{%
+  \ifthenelse{%
+    0<\value{lp@nested}%
+  }{% All is well; don't do anything.
+  }{%
+    \PackageError{logicproof}{Cannot end a subproof before it begins}{%
+      You must have a \protect\begin{subproof} before you can use %
+      \protect\end{subproof}.%
+    }%
+  }%
+  \lp@stop@proof@line%
+  \lp@cr@clines%
+  \addtocounter{lp@nested}{-1}%
+  \lp@extend@space%
+  \lp@start@proof@line%
+  \begingroup%
+  \def\@currenvir{subproof}%
+}
+\newcommand{\lp@cr}{%
+  \lp@stop@proof@line%
+  \lp@orig@arraycr%
+  \lp@extend@space%
+  \lp@start@proof@line%
+}
+\newcommand{\lp@go@up@a@line}{%
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+  \vspace{-\intersubproofvertspace}%
+}
+\newcommand{\lp@add@space}{%
+  \lp@extend@space%
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+  %\vspace{-\intersubproofvertspace}%
+}
+\newcommand{\lp@extend@space}{%
+  \vspace{-\ht\@arstrutbox}%
+  \vspace{-\dp\@arstrutbox}%
+  \vspace{\intersubproofvertspace}%
+  &%
+  \lp@continue@proof@line%
+  &%
+  \lp@stop@proof@line%
+  \lp@orig@arraycr%
+}
+\newcommand{\lp@amper}{&}
+\newcommand{\lp@start@proof@line}{%
+  \stepcounter{lp@line}%
+  \arabic{lp@line}.%
+  &%
+  \lp@continue@proof@line%
+}
+\newcommand{\lp@continue@proof@line}{%
+  \setcounter{lp@temp}{0}%
+  \whiledo{\value{lp@temp}<\value{lp@nested}}{%
+    \vline%
+    \hspace*{\subproofhorizspace}%
+    \lp@amper%
+    \stepcounter{lp@temp}%
+  }%
+  \whiledo{\value{lp@temp}<\value{lp@total@nests}}{%
+    \hspace*{\subproofhorizspace}%
+    \lp@amper%
+    \stepcounter{lp@temp}%
+  }%
+}
+\newcommand{\lp@stop@proof@line}{%
+  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
+    \addtocounter{lp@temp}{-1}%
+    \lp@amper%
+    \hspace*{\subproofhorizspace}%
+  }%
+  \whiledo{\value{lp@temp}>0}{%
+    \addtocounter{lp@temp}{-1}%
+    \lp@amper%
+    \hspace*{\subproofhorizspace}%
+    \vline%
+  }%
+}
+\newcommand{\lp@subtract@from@counter}[2]{%
+  \addtocounter{#2}{-#1}%
+}
+\newcommand{\lp@set@clines}{%
+  \setcounter{lp@cline@1}{\value{lp@nested}}%
+  \stepcounter{lp@cline@1}%
+  \setcounter{lp@cline@2}{\value{lp@total@nests}}%
+  \addtocounter{lp@cline@2}{\value{lp@total@nests}}%
+  \addtocounter{lp@cline@2}{4}%
+  \expandafter\lp@subtract@from@counter\expandafter{%
+      \value{lp@nested}}{lp@cline@2}%
+}
+\newcommand{\lp@cr@clines}{%
+  \lp@set@clines%
+  \lp@orig@arraycr%
+  \cline{\value{lp@cline@1}-\value{lp@cline@2}}%
+}
+\endinput
+%%
+%% End of file `logicproof.sty'.
diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check
index 7e98e00c1f3..76d20783ae7 100755
--- a/Master/tlpkg/bin/tlpkg-ctan-check
+++ b/Master/tlpkg/bin/tlpkg-ctan-check
@@ -226,7 +226,8 @@ my @TLP_working = qw(
     graphicx-psmin graphicxbox graphviz greek-fontenc greek-inputenc
     greekdates greektex greenpoint grfpaste
     grid grid-system gridset gtl gtrcrd gu guitar guitarchordschemes guitlogo
-  hacm hands hanging hanoi happy4th har2nat hardwrap harmony harnon-cv harpoon
+  hacm handout hands hanging hanoi
+    happy4th har2nat hardwrap harmony harnon-cv harpoon
     harvard harveyballs harvmac hatching hausarbeit-jura
     hc he-she hep hepnames
     hepparticles hepthesis hepunits here hexgame hf-tikz hfbright hfoldsty
@@ -279,7 +280,8 @@ my @TLP_working = qw(
     lipsum lisp-on-tex
     listbib listing listings listings-ext listliketab listofsymbols
     lithuanian liturg lkproof lm lm-math lmake lobster2
-    locality localloc logbox logical-markup-utils logicpuzzle logpap logreq
+    locality localloc logbox logical-markup-utils logicproof logicpuzzle
+    logpap logreq
     longnamefilelist loops lpic lplfitch lps lsc
     lshort-bulgarian lshort-chinese lshort-czech lshort-dutch lshort-english
     lshort-finnish lshort-french lshort-german lshort-italian
diff --git a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
index 1b92867c7d2..175ef53f0d2 100644
--- a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
+++ b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
@@ -23,6 +23,7 @@ depend faktor
 depend interval
 depend ionumbers
 depend isomath
+depend logicproof
 depend lplfitch
 depend mathcomp
 depend mattens
diff --git a/Master/tlpkg/tlpsrc/logicproof.tlpsrc b/Master/tlpkg/tlpsrc/logicproof.tlpsrc
new file mode 100644
index 00000000000..e69de29bb2d
--- /dev/null
+++ b/Master/tlpkg/tlpsrc/logicproof.tlpsrc