Bioinformatik Blog

Dieses Semester steht “Mathematische Logik” auf dem Plan. Dies ist eine der Veranstaltungen, zu denen es sich lohnt eine saubere `Mitschrift `_ anzufertigen. Das Problem dabei ist nur, dass im Bereich der Logik sehr viele merkwürdige Zeichen verwendet werden, die man dann auf dem Computer erstmal dargestellt bekommen muss. Da ich meine Mitschriften in LaTeX schreibe (unter Zuhilfenahme des großartigen Programms LyX) schreibe, will ich hier mal kurz erklären, wie man einige der seltsam anmutenden Zeichen und Notationen dort gesetzt bekommt.

Sonderzeichen

In der mathematischen Notation der Logik werden Sonderzeichen gebraucht, bspw. um Auswertungsfunktionen zu notieren oder die logische Äquivalenz zweier Ausdrücke aufzuschreiben:

Standardmäßig kann LaTeX solche Zeichen nicht setzen. Man kann es ihm aber sehr einfach beibringen, indem man das Paket mathabx installiert, das man bei CTAN herunterladen kann. Dieses unterstützt gigantisch viele Zeichen, wie man der Übersicht [PDF] entnehmen kann.

Beweise

In den unterschiedlichen Kalkülen, die man in der Logik behandelt, hat sich eine besondere Schreibweise für Beweise eingebürgert. Von Hand sind diese recht leicht zu schreiben, am Computer werden sie aber schnell zu einer Qual.

Hier kann man sich des Pakets **proof** bedienen, das man ebenfalls bei CTAN bekommen kann. Nach der Installation und Einbindung in sein LaTeX Dokument kann man nun folgende Befehle benutzen:

• \infer
• \infer[Beschriftung]
• \infer*
• \infer*[Beschriftung]

Dabei ist die Folgerung immer das, was unter dem Strich steht, und der Ursprung das darüber. Wenn man neben dem Beweis eine Annotation haben möchte, kann man sich der eckigen Klammern bedienen. Setzt man hinter den Befehl einen Stern, wird statt der horizontalen Trennlinie eine vertikale gepunktete Linie dargestellt.

Um größere Beweise zusammenzubauen, muss man mehrere dieser Anweisungen in einander stapeln. Hat man mehrere Ursprungsterme, muss man diese mit einem Ampersand (&) trennen. Ein kleines Beispiel:

\\infer[\\rightarrow RAA]{\\psi}{
  \\infer{\\bot}{
    \\neg \\varphi &
    \\varphi
  }
}

Erhalten würde man damit folgende Darstellung:

Gliederungsbäume

Manchmal zerlegt man Aussagen mittels eines Gliederungsbaums. Um diese darzustellen, gibt es eine ganze Reihe von brauchbaren Paketen. Ich persönlich bevorzuge inzwischen zu diesem Zweck synttree, das relativ einfach zu bedienen ist. Man muss einfach nur die Verschachtelung des Baums in folgender Art und Weise aufschreiben:

\\synttree[$\\wedge$ [$\\neg$ [a]] [$\\vee$ [e] [f]]]

Dabei bekommt man von LaTeX dann folgendes Ergebnis: