Generate TikZ code for a semantic tableau using Python objects

generate_tikz_tableau.py

from enum import Enum
from typing import List, Dict, Optional

header = r"""
\begin{center}
    \begin{tikzpicture}
        \tikzset{level distance=4\baselineskip}
        \Tree
"""

footer = r"""
    \end{tikzpicture}
\end{center}
"""


class Rule(Enum):
    EPSILON = 0
    ALPHA = 1
    BETA = 2
    CLOSED_DEAD = 3
    CLOSED_ATOM = 4


class Node:
    def __init__(
        self,
        exprs: Dict[int, str],
        rule_type: Rule = Rule.CLOSED_DEAD,
        rule_selection: int = -1,
        children: Optional[List["Node"]] = None,
    ):
        self.exprs = exprs
        self.rule_type = rule_type
        self.rule_selection = rule_selection
        self.children = children if children is not None else []

    def expression_string(self) -> str:
        if len(self.exprs) == 1:
            expr_num, expr_str = next(iter(self.exprs.items()))
            return (
                r".\tableauNode{"
                + str(expr_num)
                + r"}"
                + "%\n"
                + r"  {$"
                + expr_str
                + r"$}"
            )
        else:
            expr_list = [
                r"\tableauNode{" + str(num) + r"}{$" + expr + r"$} \\"
                for num, expr in self.exprs.items()
            ]
            expr_list[-1] = expr_list[-1][:-3]
            return (
                r".\node[align=center]{" + "\n" + r"  " + "\n".join(expr_list) + r"  };"
            )

    def __str__(self):
        return self._generate_tikz(indent=4)

    def _generate_tikz(self, indent: int) -> str:
        indent_str = " " * indent
        node_str = self.expression_string()

        if self.rule_type == Rule.BETA:
            node_str += (
                "\n"
                + indent_str
                + r"  \edge node[auto=left,pos=0.4]{{\hspace*{-9pt}\tt $\beta$ on "
                + str(self.rule_selection)
                + "}};"
            )
        elif self.rule_type == Rule.ALPHA:
            node_str += (
                "\n"
                + indent_str
                + r"  \edge node[auto=left]{{\tt $\alpha$ on "
                + str(self.rule_selection)
                + "}};"
            )
        elif self.rule_type == Rule.EPSILON:
            node_str += (
                "\n"
                + indent_str
                + r"  \edge node[auto=left]{{\tt $\varepsilon$ on "
                + str(self.rule_selection)
                + "}};"
            )

        result = indent_str + "[" + node_str

        if self.children:
            for child in self.children:
                result += "\n" + child._generate_tikz(indent + 2)

        elif self.rule_type == Rule.CLOSED_DEAD:
            result += "\n" + (indent_str + "  ") + r"[.{\tableaux} ]"
        elif self.rule_type == Rule.CLOSED_ATOM:
            result += "\n" + (indent_str + "  ") + r"[.{\xspace\ding{51}\xspace} ]"

        result += "\n" + indent_str + "]"

        return result


def generate_tableau_latex(root_node: Node) -> str:
    """
    Combines the header, the generated tree, and the footer.
    """
    return header + root_node.__str__() + "\n" + footer


if __name__ == "__main__":
    # Example: a tableau for a satisfiable WFF
    sample_input = Node(
        exprs={1: r"(p \land (\neg p \lor r)) \lor \neg(q \lor \neg q)"},
        rule_type=Rule.BETA,
        rule_selection=1,
        children=[
            Node(
                exprs={
                    2: r"(p\land (\neg p\lor r)",
                },
                rule_type=Rule.ALPHA,
                rule_selection=2,
                children=[
                    Node(
                        exprs={3: r"p", 4: r"\neg p\lor r"},
                        rule_type=Rule.BETA,
                        rule_selection=4,
                        children=[
                            Node(exprs={5: r"\neg p"}, rule_type=Rule.CLOSED_DEAD),
                            Node(exprs={6: r"r"}, rule_type=Rule.CLOSED_ATOM),
                        ],
                    )
                ],
            ),
            Node(
                exprs={7: r"\neg (q \lor \neg q)"},
                rule_type=Rule.ALPHA,
                rule_selection=7,
                children=[
                    Node(
                        exprs={8: r"\neg q", 9: r"\neg\neg q"},
                        rule_type=Rule.EPSILON,
                        rule_selection=9,
                        children=[Node(exprs={10: r"q"}, rule_type=Rule.CLOSED_DEAD)],
                    )
                ],
            ),
        ],
    )
    print(generate_tableau_latex(sample_input))

Instructions

To use this, make sure you include the below in your preamble:

\usepackage{xspace}
\usepackage{pifont}
\usepackage{tikz}
\usepackage{tikz-qtree}
\def\tableaux{\xspace\ding{55}\xspace}
\def\tableauNode#1#2{(#1) \hspace{1pt} #2}

Example

See the example included above.

When rendered, the output yields this diagram: