LLWiki LaTeX Style
From LLWiki
(Difference between revisions)
(→Mathematical notations: \biorth and \triorth added) |
m (→Proof trees: typo) |
||
(7 intermediate revisions by 2 users not shown) | |||
Line 44: | Line 44: | ||
| <math>A\limp B</math> |
| <math>A\limp B</math> |
||
| <pre>A\limp B</pre> |
| <pre>A\limp B</pre> |
||
+ | |- |
||
+ | | <math>A\nlimp B</math> |
||
+ | | <pre>A\nlimp B</pre> |
||
+ | |- |
||
+ | | <math>A\limpinv B</math> |
||
+ | | <pre>A\limpinv B</pre> |
||
+ | |- |
||
+ | | <math>A\nlimpinv B</math> |
||
+ | | <pre>A\nlimpinv B</pre> |
||
|- |
|- |
||
| <math>A\linequiv B</math> |
| <math>A\linequiv B</math> |
||
| <pre>A\linequiv B</pre> |
| <pre>A\linequiv B</pre> |
||
+ | |- |
||
+ | | <math>A\nlinequiv B</math> |
||
+ | | <pre>A\nlinequiv B</pre> |
||
|- |
|- |
||
| <math>\shpos A</math> |
| <math>\shpos A</math> |
||
Line 87: | Line 99: | ||
| <pre>\set{x}{P}</pre> |
| <pre>\set{x}{P}</pre> |
||
|- |
|- |
||
+ | | <math>\powerset{A}</math> |
||
+ | | <pre>\powerset{A}</pre> |
||
+ | |- |
||
+ | | <math>\finpowerset{A}</math> |
||
+ | | <pre>\finpowerset{A}</pre> |
||
+ | |- |
||
+ | | <math>\mulset{A}</math> |
||
+ | | <pre>\mulset{A}</pre> |
||
+ | |- |
||
+ | | <math>\finmulset{A}</math> |
||
+ | | <pre>\finmulset{A}</pre> |
||
+ | |- |
||
+ | | <math>\Bot</math> |
||
+ | | <pre>\Bot</pre> |
||
+ | |- |
||
+ | | <math>A\Perp B</math> |
||
+ | | <pre>A\Perp B</pre> |
||
+ | |- |
||
+ | | <math>A\pinj B</math> |
||
+ | | <pre>A\pinj B</pre> |
||
+ | |- |
||
+ | | <math>\inner{A}{B}</math> |
||
+ | | <pre>\inner{A}{B}</pre> |
||
+ | |- |
||
+ | | <math>\Inner{A}{B}</math> |
||
+ | | <pre>\Inner{A}{B}</pre> |
||
+ | |- |
||
+ | |} |
||
+ | |||
+ | == Proof trees == |
||
+ | |||
+ | Proof trees are described using a postfix syntax and terminated with <tt>\DisplayProof</tt> |
||
+ | |||
+ | {| border="1" cellpadding="10" cellspacing="0" |
||
+ | |- |
||
+ | | '''Description''' |
||
+ | | '''Command''' |
||
+ | | '''Example''' |
||
+ | | '''LaTeX source''' |
||
+ | |- |
||
+ | | Axiom node <br /> (for hypotheses) |
||
+ | | <pre>\AxRule</pre> |
||
+ | | <math> |
||
+ | \AxRule{\vdash A} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{\vdash A} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Nullary rule <br /> (for logical axioms) |
||
+ | | <pre>\NulRule</pre> |
||
+ | | <math> |
||
+ | \NulRule{A \vdash A} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \NulRule{A \vdash A} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Unary rule |
||
+ | | <pre>\UnaRule</pre> |
||
+ | | <math> |
||
+ | \AxRule{\vdash \wn\Gamma, A} |
||
+ | \UnaRule{\vdash \wn\Gamma, \oc A} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{\vdash \wn\Gamma, A} |
||
+ | \UnaRule{\vdash \wn\Gamma, \oc A} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Binary rule |
||
+ | | <pre>\BinRule</pre> |
||
+ | | <math> |
||
+ | \AxRule{\Gamma\vdash A} |
||
+ | \AxRule{\Delta,A\vdash C} |
||
+ | \BinRule{\Gamma,\Delta\vdash C} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{\Gamma\vdash A} |
||
+ | \AxRule{\Delta,A\vdash C} |
||
+ | \BinRule{\Gamma,\Delta\vdash C} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Ternary rule |
||
+ | | <pre>\TriRule</pre> |
||
+ | | <math> |
||
+ | \AxRule{\vdash A} |
||
+ | \AxRule{\vdash B} |
||
+ | \AxRule{\vdash C} |
||
+ | \TriRule{\vdash A\land B\land C} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{\vdash A} |
||
+ | \AxRule{\vdash B} |
||
+ | \AxRule{\vdash C} |
||
+ | \TriRule{\vdash A\land B\land C} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Label <br /> (before any of the above) |
||
+ | | <pre>\LabelRule</pre> |
||
+ | | <math>\AxRule{\Gamma\vdash A} |
||
+ | \AxRule{\Delta,A\vdash C} |
||
+ | \LabelRule{\rulename{cut}} |
||
+ | \BinRule{\Gamma,\Delta\vdash C} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{\Gamma\vdash A} |
||
+ | \AxRule{\Delta,A\vdash C} |
||
+ | \LabelRule{\rulename{cut}} |
||
+ | \BinRule{\Gamma,\Delta\vdash C} |
||
+ | \DisplayProof</pre> |
||
+ | |- |
||
+ | | Proof ellipsis<br /> ''(two arguments !)'' |
||
+ | | <pre>\VdotsRule</pre> |
||
+ | | <math> |
||
+ | \AxRule{[A]} |
||
+ | \VdotsRule{\pi}{B} |
||
+ | \UnaRule{A\imp B} |
||
+ | \DisplayProof</math> |
||
+ | | <pre> |
||
+ | \AxRule{[A]} |
||
+ | \VdotsRule{\pi}{B} |
||
+ | \UnaRule{A\imp B} |
||
+ | \DisplayProof</pre> |
||
|} |
|} |
Latest revision as of 14:51, 27 June 2013
[edit] 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\nlimp B | |
A\limpinv B | |
A\nlimpinv B | |
A\linequiv B | |
A\nlinequiv 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 | |
A\pinj B | |
\inner{A}{B} | |
\Inner{A}{B} |
[edit] 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 |