☰

Logicproof 包和公理证明，布局问题

tag-icon • tag-icon tables layout logic proof-package logicproof
Logicproof 包和公理证明，布局问题

我正在使用 logicproof 包以公理形式编写证明。问题是，如果证明的一行太长，整个块就会超出页边距。

以下是一个例子：

以下是代码：

\documentclass[12pt,a4paper,oneside, onehalfspacing openright]{book}
\usepackage{logicproof}
\usepackage{amsmath, amsthm, amssymb, amsfonts}

\begin{document}
\begin{logicproof}{0}
    \vdash \textbf{I} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3} \land \dagger^{*}, \neg V3}) & from $\spadesuit$\\
    \textbf{K2} \vdash \textbf{K} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3}}) & instance of \textbf{K2}\\
    \dagger^{**} \vdash \textbf{K}(\overline{\dagger^{*}}) & $\dagger^{**}$\\
    \textbf{K3} \vdash  \textbf{I} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3} \land \dagger^{*}, \neg V3}) \land  \textbf{K}_{s} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3}}) \land \textbf{K}_{s}(\overline{\dagger^{*}}) \rightarrow \textbf{K}_{s} (\overline{\neg V3})& intance of \textbf{K3}\\
    \textbf{K2, K3}, \dagger^{**} \vdash \textbf{K}_{s} (\overline{\neg V3}) & MP from 1, 2, 3, 4\\
    \vdash  \textbf{K}_{s} (\overline{\neg V3}) \rightarrow V3 &logic from V3\\
    \textbf{K2, K3}, \dagger^{**} \vdash V3 &  MP from 5, 6\\
    \textbf{K1, K2, K3}, \dagger^{*}, \dagger^{**} \vdash  V3 \land \neg V3 & from 7 and $\spadesuit$
\end{logicproof}    
\end{document}

当然，我尝试过缩小字体大小，但这不是一个合适的解决方案。

答案1

以下是如何重新定义logicproof环境以允许第二列换行的方法。（如果最后一列的文本长度和/或文本宽度发生变化，则应调整第二列的宽度。不幸的是，我无法tabularx在这里正常工作。）

在此处输入图片描述

\documentclass[12pt,a4paper,oneside, onehalfspacing openright]{book}
\usepackage{logicproof}
\usepackage{amsmath, amsthm, amssymb, amsfonts}

\makeatletter
\renewenvironment{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@{~~~}>{\raggedright\arraybackslash\(\displaystyle}p{9cm}<{\)}@{~~~~}l}}%
  }{%
    \def\lp@tab@format%
        {{r@{~~~}*{#1}{l}@{~}>{\raggedright\arraybackslash\(\displaystyle}p{9cm}<{\)}@{~~~~}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}%
  }
}
\makeatother

\begin{document}
\begin{logicproof}{0}
    \vdash \textbf{I} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3} \land \dagger^{*}, \neg V3}) & from $\spadesuit$\\
    \textbf{K2} \vdash \textbf{K} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3}}) & instance of \textbf{K2}\\
    \dagger^{**} \vdash \textbf{K}(\overline{\dagger^{*}}) & $\dagger^{**}$\\
    \textbf{K3} \vdash  \textbf{I} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3} \land \dagger^{*}, \neg V3}) \land  \textbf{K}_{s} (\overline{\textbf{K1} \land \textbf{K2} \land \textbf{K3}}) \land \textbf{K}_{s}(\overline{\dagger^{*}}) \rightarrow \textbf{K}_{s} (\overline{\neg V3})& intance of \textbf{K3}\\
    \textbf{K2, K3}, \dagger^{**} \vdash \textbf{K}_{s} (\overline{\neg V3}) & MP from 1, 2, 3, 4\\
    \vdash  \textbf{K}_{s} (\overline{\neg V3}) \rightarrow V3 &logic from V3\\
    \textbf{K2, K3}, \dagger^{**} \vdash V3 &  MP from 5, 6\\
    \textbf{K1, K2, K3}, \dagger^{*}, \dagger^{**} \vdash  V3 \land \neg V3 & from 7 and $\spadesuit$
\end{logicproof}    
\end{document}

相关内容