Does exist a package for Lemmon style proof in Logic? something like:
http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-bau.html
thanks
[Tex/LaTex] lemmon style proof for logic
logic
Related Solutions
Here is a first approach to a smaller logic circuit, with more compact positioning, and colored label text.
\documentclass{article}
\usepackage{fullpage}
\usepackage[american]{circuitikz}
\usetikzlibrary{positioning}
\begin{document}
\begin{circuitikz}[every label/.style={blue}]
\draw
% draw And1 gate with label then Not1 gate with label
(3,3) node[and port] (myand1) {}
(-1,3.3) node[label=left:$p$] {} -- (myand1.in 1)
(myand1.out) node[label=right:$p \wedge \neg r$] {}
(0,2.75) node[scale=0.7,not port] (mynot1) {}
(-1,2.75)node[label=left:$r$] {} -- (mynot1.in)
(mynot1.out) node[label=above:$\neg r$] {}
(mynot1.out) -- (myand1.in 2)
% draw And2 gate with label then Not2 gate with label
(3,1) node[and port] (myand2) {}
(-1,0.75) node[label=left:$r$] {} -- (myand2.in 2)
(myand2.out) node[label=right:$\neg q \wedge r$] {}
(0,1.3) node[scale=0.7,not port] (mynot2) {}
(-1,1.3) node[label=left:$q$] {} -- (mynot2.in)
(mynot2.out) node[label=above:$\neg q$] {}
(mynot2.out) -- (myand2.in 1)
% draw Or gate with inputs and output label
(6,2) node[or port] (myor) {}
(myand1.out) |- (myor.in 1)
(myand2.out) |- (myor.in 2)
(myor.out) -- (8,2) node[label=above:$(p \wedge \neg r) \vee (\neg q \wedge r)$] {}
;
\end{circuitikz}
\end{document}
You can increase \subproofhorizspace (the extra pair of braces in my code keep the change local) and then use \llap for the variable:
\documentclass{article}
\usepackage{logicproof}
\begin{document}
{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
\forall x \, (P(x) \to Q(x)) & premise \\
\forall x \, P(x) & premise \\\hspace*{-30pt}
\begin{subproof}
\llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
Q(x_0) & $\to \mathrm{e}$ 3, 4
\end{subproof}
\forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}
\end{document}
The above solution will change the horizontal separation on both sides; if you want individual control, here's one possibility:
\documentclass{article}
\usepackage{logicproof}
\newlength\subproofhorizspaceright
\setlength\subproofhorizspaceright{\subproofhorizspace}
\makeatletter
\renewcommand{\lp@stop@proof@line}{%
\whiledo{\value{lp@temp}>\value{lp@nested}}{%
\addtocounter{lp@temp}{-1}%
\lp@amper%
\hspace*{\subproofhorizspaceright}%
}%
\whiledo{\value{lp@temp}>0}{%
\addtocounter{lp@temp}{-1}%
\lp@amper%
\hspace*{\subproofhorizspaceright}%
\vline%
}%
}
\makeatother
\begin{document}
{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
\forall x \, (P(x) \to Q(x)) & premise \\
\forall x \, P(x) & premise \\\hspace*{-30pt}
\begin{subproof}
\llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
Q(x_0) & $\to \mathrm{e}$ 3, 4
\end{subproof}
\forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}
\end{document}
Now there's \subproofhorizspace controlling the space to the left and \subproofhorizspaceright for the space to the right.
Best Answer
There is a package which is not on CTAN but can be found at: http://phloxgroup.wordpress.com/2010/03/22/lemmon-style-natural-deduction-proofs-in-latex/ (for some reason¹, the author saved the file as a .doc file, just save as .sty file and it will work).
I haven't thoroughly tested the package, but you can do things like:
(example taken from the manual)
You may also want to take a look at the packages listed at: http://www.logicmatters.net/latex-for-logicians/ maybe you'll find something interesting
--
¹Actually, the reason is explained in the blog