☰

BEARBEITEN

tag-icon • tag-icon tikz-trees forest trees logic proof-package
BEARBEITEN

Ich muss in meinem Dokument einige semantische Tableaus setzen, die dem folgenden Beispiel ähneln.

Semantisches Tableau

Meine erste Idee war, tikzdies zu verwenden, also habe ich das folgende Monster erstellt:

Hässlicher Baum

\documentclass[convert]{standalone}
\usepackage{tikz,amssymb}
\usetikzlibrary{positioning}
\newcommand{\lnec}{\Box}
\begin{document}
  \begin{tikzpicture}[scale=2]
    \node[label=right:$(\lnec p\to\lnec q)\to\lnec(p\to q)$] (n1) {$\circ_1$};
    \node[label=left:$\lnec p\to\lnec q$, label=right:$\lnec(p\to q)$, below=of n1] (n2) {$\circ_1$};
    \node[label=left:$\lnec q$, label=right:$\lnec(p\to q)$, below left=of n2] (n3) {$\circ_1$};
    \node[label=right:{$\lnec p, \lnec(p\to q)$}, below right=of n2] (n4) {$\circ_1$};
    \node[label=left:$q$, label=right:$\lnec(p\to q)$, below=of n3] (n5) {$\circ_2$};
    \node[label=right:$p$, below left=of n4] (n6) {$\circ_3$};
    \node[label=right:$p\to q$, below right=of n4] (n7) {$\circ_4$};
    \node[label=left:$p$, label=right:$q$, below=of n7] (n8) {$\circ_4$};

    \draw[-] (n1) to (n2);
    \draw[-] (n2) to (n3);
    \draw[-] (n2) to (n4);
    \draw[-, dotted] (n3) to (n5);
    \draw[-, dotted] (n4) to (n6);
    \draw[-, dotted] (n4) to (n7);
    \draw[-] (n7) to (n8); 
  \end{tikzpicture}
\end{document}

Es ist klar, dass dies nicht das gewünschte Ergebnis ist. Die Kanten sollten unterhalb beginnen und oberhalb der\circ s enden und sie sollten rechte Winkel haben, sodass das Diagramm etwas komprimiert werden kann.

Das Zeichnen dieser Art von Diagrammen ist für mich völliges Neuland. Können Sie mir also einige nützliche Richtlinien geben? Haben Sie Tipps oder Tricks zum Erstellen dieser semantischen Tableaus im Allgemeinen? Sind Pakete wie forestoder qtree„produce“ für diese Art von Bäumen einfacher zu verwenden?

Bearbeiten: Die Antwort von @cfr ist vielversprechend, daher würde ich gerne an forestseinem Stil arbeiten und ihn verfeinern tableaux. Ich habe in den letzten zwei Tagen versucht, es selbst zu tun, aber es foreststellte sich für einen Anfänger wie mich als unmöglich heraus, alle erweiterten Optionen in der Dokumentation zu verstehen. Daher würde ich der Person, die die Feinabstimmung für mich vornehmen kann, gerne eine Belohnung aussprechen. Das bedeutet

  • der Abstand zwischen WFF und \circSeparator sollte verkleinert werden,
  • die Kanten sollten mit der Mitte der \circTrennzeichen ausgerichtet sein, wobei die möglichen Indizes ignoriert werden,
  • das obige sollte auch funktionieren, wenn kein Index für das \circTrennzeichen angegeben ist.

Antwort1

Diese Antwort verwendet einen völlig anderen Ansatz, da der Code aus der ursprünglichen Version der Frage leider verloren gegangen ist. Sie ist möglicherweise weniger hilfreich, da sie nicht auf diesem Code basiert, aber ich werde sie hier lassen, da sie irgendwann für jemanden von Nutzen sein könnte.

Hier ist ein grundlegender Forest-Stil tableaux, der für diese Art von Diagramm verwendet werden könnte.

Das Problem bei der Verwendung labelbesteht darin, dass es bei der Positionierung der Knoten relativ zueinander nicht berücksichtigt wird. tableauxerstellt stattdessen zusätzliche Knoten für diesen Inhalt, die zusammen mit dem „Haupt“-Knoten angegeben werden. Dadurch ist es möglich, die Dinge korrekt am „Haupt“-Kreis auszurichten und gleichzeitig ausreichend Platz für die WFFs zu lassen.

Der einzige wirkliche Nachteil dabei ist, dass ein zusätzlicher phantomStammknoten erstellt werden muss, da wir sonst mit 2 oder 3 Wurzeln enden würden (dem Hauptknoten auf der obersten Ebene und WFFs auf jeder Seite). Das ist nicht möglich. Daher der Phantom-Stammknoten.

Wenn Sie viele dieser Aktionen ausführen, können Sie das Hinzufügen des Phantom-Roots vermeiden, indem Sie eine neue Umgebung erstellen, die dies automatisch erledigt. (Das environPaket kann hierfür mit einem benutzerdefinierten Namen für den Umgebungskörper verwendet werden.)

edgesZur Bereitstellung des Stils wird die Bibliothek von Forest verwendet forked edges.

Die Feinabstimmung bleibt dem Leser überlassen. Beispielsweise könnte es besser aussehen, die Geschwisterabstände anzupassen, um die WFFs näher heranzubringen.

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={F}{},
  declare toks={T}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      delay={%
        content/.wrap value={\circ_{##1}},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

Bilder

BEARBEITEN

Dies geht auf die 3 der Frage hinzugefügten Desiderate ein. Wir vermeiden die Auswirkung der Indizes auf die Ausrichtung, indem wir sie als Beschriftungen und nicht als Teil der Knoten darstellen. Wir passen den Abstand zu den WFFs an, bevor wir den Baum zeichnen, da wir die Geschwisterabstände nicht allgemein verringern möchten, sondern nur den Abstand zwischen den Kreisen und den zugehörigen WFFs. Dies ist mit und ohne Indizes in Ordnung.

Abhängig von Ihrer tatsächlichen Nutzung, Schriftfamilie und -größe usw. möchten Sie möglicherweise die in den Anpassungen verwendeten bestimmten Abmessungen anpassen. Dies sind -3.5ptund 3.5ptfür die Indizes und 7.5ptund -7.5ptfür die WFFs im MWE unten.

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p
              [99, F=X!, T=XX!!
                [, F=XXX!!!, T=XXXX!!!!]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

optimierte Version

BEARBEITEN BEARBEITEN

Wie in einem Kommentar erwähnt, hat mein Edit dazu geführt, dass die Closures verschwunden sind. Das liegt daran, dass sie mit erstellt wurden labelund die Nummern oben rechts in den Knoten ebenfalls mit hinzugefügt wurden label. Obwohl die Labels an verschiedenen Stellen angefordert werden und in normalem TikZ-Code in Ordnung wären, definiert Forest labelso, dass nur eines pro Knoten zulässig ist. Außerdem:label Auchüberschreibt alle zuvor mit tikzoder angegebenen Anmerkungen pin. Von forest.sty:

 label/.style={tikz={\path[late options={%
        name=\forestoption{name},label={#1}}];}},
 pin/.style={tikz={\path[late options={%
        name=\forestoption{name},pin={#1}}];}},

Jeder Aufruf tikzüberschreibt alle vorherigen Einstellungen. Daher sammelt sich kein Code an, sondern ersetzt vorhandenen Code.

Ich bin mir nicht sicher, welchen Grund der Autor für diese Wahl hatte, daher bin ich mir nicht ganz sicher, wie ich das am besten angehen soll. Eine Möglichkeit wäre, für die Zahlen zu verwenden , was die Verwendung von im Baum selbst afterthoughtermöglichen sollte . In diesem Fall könnten wir die Zahlen jedoch nicht als TikZ s angeben, ohne im Wesentlichen den Code zu reproduzieren, den Forest von vornherein für verwendet. Da dies keinen Vorteil zu bringen scheint, ist es verlockend, stattdessen neu zu definieren, indem der Präambel des Dokuments der folgende Code hinzugefügt wird:labellabellabellabel

\forestset{% Sašo Živanović won't like this ...
  label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
}

Hier +ist, was den Unterschied macht. Jetzt labelwerden s akkumuliert, anstatt sich gegenseitig und/oder vorherige Verwendungen von pin, tikzoder zu überschreiben tikz+. Wie bereits erwähnt, kann ich mir nicht vorstellen, dass dies die Art von Dingen ist, die ich tun soll, also empfehle ich es nicht, auch wenn es funktioniert:

Closures mit Hack wiederherstellen

Eine komplexere Alternative besteht darin, Folgendes zu verwenden:

\forestset{%
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  }
}

Die Platzierung der Zahlen erfolgt dann einfach durch my labelanstelle von label. Komplette Konfiguration:

\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}

was zum gleichen Ergebnis wie oben führt, ohne den Stil von Forest neu zu definieren label.

verwandte Informationen