LLWiki LaTeX Style
From LLWiki
Revision as of 16:58, 6 July 2009 by Lionel Vaux (Talk | contribs)
Mathematical notations
A\orth | |
A\biorth | |
A\triorth | |
A\tens B | |
A\parr B | |
A\plus B | |
A\with B | |
\one | |
\bot | |
\zero | |
\top | |
\oc A | |
\wn A | |
A\limp B | |
A\linequiv B | |
\shpos A | |
\shneg A | |
\shift A | |
\pg A | |
A\imp B | |
\sem{A} | |
\web{A} | |
A\coh B | |
A\scoh B | |
A\incoh B | |
A\sincoh B | |
A\cliq B | |
\set{x}{P} | |
\powerset{A} | |
\finpowerset{A} | |
\mulset{A} | |
\finmulset{A} | |
\Bot | |
A\Perp B |
Proof trees
Proof trees are described using a postfix syntax and terminated with \DisplayProof
Description | Command | Example | LaTeX source |
Axiom node (for hypotheses) |
\AxRule |
\AxRule{\vdash A} \DisplayProof | |
Nullary rule (for logical axioms) |
\NulRule |
\NulRule{A \vdash A} \DisplayProof | |
Unary rule | \UnaRule |
\AxRule{\vdash \wn\Gamma, A} \UnaRule{\vdash \wn\Gamma, \oc A} \DisplayProof | |
Binary rule | \BinRule |
\AxRule{\Gamma\vdash A} \AxRule{\Delta,A\vdash C} \BinRule{\Gamma,\Delta\vdash C} \DisplayProof | |
Ternary rule | \TriRule |
\AxRule{\vdash A} \AxRule{\vdash B} \AxRule{\vdash C} \TriRule{\vdash A\land B\land C} \DisplayProof | |
Label (before any of the above) |
\LabelRule |
\AxRule{\Gamma\vdash A} \AxRule{\Delta,A\vdash C} \LabelRule{\rulename{cut}} \BinRule{\Gamma,\Delta\vdash C} \DisplayProof | |
Proof ellipsis (two arguments !) |
\VdotsRule |
\AxRule{[A]} \VdotsRule{\pi}{B} \UnaRule{A\imp B} \DisplayProof |
UNIQ6aadea181b3efc3e-math-00000059-QINU