在 LaTeX 中编写线性时序逻辑

Question

我正在用 LaTeX 编写一些 LTL（线性时间逻辑）语句，但在网上找不到任何软件包或有关此操作的信息。如能得到任何帮助，我将不胜感激。

Answer 1

以下是一些有用的符号

\documentclass{article}
\usepackage{amsmath,amssymb}
\pagestyle{empty}
\begin{document}
\renewcommand{\arraystretch}{2}

\begin{tabular}[t]{rl|rl}%
      \verb=\lnot=   & $ \lnot $ & \\
      \verb=\square= & $\square$ & \verb=\lozenge= & $\lozenge$ \\
      \verb=\vee=    & $\vee $   & \verb=\wedge=   & $\wedge$  \\
      \verb=\vdash=  & $\vdash$  & \verb=\models=  & $\models$ \\
\end{tabular}

\end{document}

Answer 2

将 DRY 应用于 A.Ellet 的答案。

\documentclass[preview]{standalone}
\usepackage{amsmath,amssymb}

\renewcommand{\arraystretch}{2}

\def\x#1{\texttt{\expandafter\string\csname#1\endcsname}&\expandafter$\csname#1\endcsname$}


\begin{document}
\begin{tabular}[t]{rl|rl}%
    \x{lnot}    & \multicolumn{2}{c}{none}\\
    \x{square}  & \x{lozenge}\\
    \x{vee}     & \x{wedge}\\
    \x{vdash}   & \x{models}\\
\end{tabular}
\end{document}

Answer 3

有LTL字体 斯坦福的 LaTeX 包，为线性时间逻辑提供命令和字体。

最近有一个立特LaTeX 包（此文章正在进行中）支持字母运算符 F、G 等，以及符号运算符 <>、[] 等。请注意，此包包含前一个作为选项。

有圆圈CTAN 上的包，为下一个操作员提供改进的符号。

Answer 4

如果你像我一样，使用你知道的名称可能会在编写公式时有所帮助 - TeX 让你定义命令，这样你就可以将符号“映射”到你知道的单词：

\def\always{\square}
\def\next{\circ}
\def\eventually{\diamond}
\def\and{\wedge}
\def\or{\vee}
\def\until{\mathcal{U}}

这使你可以编写如下内容：

\always ( a_0 \implies (( \lnot a_2 \and \lnot a_3 ) \until a_1 ) \or ( \lnot a_2 \and \lnot a_3 ))

代替 ：

\square ( a_0 \implies (( \lnot a_2 \wedge \lnot a_3 ) \mathcal{U} a_1 ) \vee ( \lnot a_2 \wedge \lnot a_3 ))

并得到相同的结果：