LLWiki LaTeX Style

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(→‎Proof trees: \VdotsRule added)
(→‎Proof trees: describe all available commands for proof trees)
Line 109: Line 109:
 
== Proof trees ==
  
== 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>
  +
|}
 
<math>
  
<math>
−
\AxRule{{}\vdash\Gamma,A,B,C}
  
−
\VdotsRule{\pi}{{}\vdash\Gamma,A\parr B\parr C}
  
−
\NulRule{{}\vdash A,A\orth}
  
−
\NulRule{{}\vdash B,B\orth}
  
−
\NulRule{{}\vdash C,C\orth}
  
−
\TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth}
  
−
\LabelRule{\rulename{cut}}
  
−
\BinRule{{}\vdash\Gamma,A,B,C}
  
−
\UnaRule{{}\vdash\Gamma,A\parr B\parr C}
  
−
\DisplayProof
  
−
</math>
  

Revision as of 16:58, 6 July 2009

Mathematical notations

A\orth 
A\orth
A\biorth 
A\biorth
A\triorth 
A\triorth
A\tens B 
A\tens B
A\parr B 
A\parr B
A\plus B 
A\plus B
A\with B 
A\with B
\one 
\one
\bot 
\bot
\zero 
\zero
\top 
\top
\oc A 
\oc A
\wn A 
\wn A
A\limp B 
A\limp B
A\linequiv B 
A\linequiv B
\shpos A 
\shpos A
\shneg A 
\shneg A
\shift A 
\shift A
\pg A 
\pg A
A\imp B 
A\imp B
\sem{A} 
\sem{A}
\web{A} 
\web{A}
A\coh B 
A\coh B
A\scoh B 
A\scoh B
A\incoh B 
A\incoh B
A\sincoh B 
A\sincoh B
A\cliq B 
A\cliq B
\set{x}{P} 
\set{x}{P}
\powerset{A} 
\powerset{A}
\finpowerset{A} 
\finpowerset{A}
\mulset{A} 
\mulset{A}
\finmulset{A} 
\finmulset{A}
\Bot 
\Bot
A\Perp B 
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 
  \AxRule{\vdash A}
  \DisplayProof
Nullary rule
(for logical axioms) 
\NulRule
 \NulRule{A \vdash A} \DisplayProof 
  \NulRule{A \vdash A}
  \DisplayProof
Unary rule 
\UnaRule
 \AxRule{\vdash \wn\Gamma, A} \UnaRule{\vdash \wn\Gamma, \oc A} \DisplayProof 
  \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 
  \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 
  \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 
  \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 
  \AxRule{[A]}
  \VdotsRule{\pi}{B}
  \UnaRule{A\imp B}
  \DisplayProof

UNIQ34d44dbd2e7bf3ca-math-00000059-QINU

Retrieved from "http://llwiki.ens-lyon.fr/mediawiki/index.php?title=LLWiki_LaTeX_Style&oldid=405"
Personal tools