LLWiki LaTeX Style

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(example of proof tree)
m (Proof trees: typo)
 
(5 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 86: Line 98:
 
| <math>\set{x}{P}</math>
 
| <math>\set{x}{P}</math>
 
| <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>
 
| <math>\Bot</math>
Line 92: Line 116:
 
| <math>A\Perp B</math>
 
| <math>A\Perp B</math>
 
| <pre>A\Perp B</pre>
 
| <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>
 
|-
 
|-
 
|}
 
|}
Line 97: Line 130:
 
== Proof trees ==
 
== Proof trees ==
   
<math>
+
Proof trees are described using a postfix syntax and terminated with <tt>\DisplayProof</tt>
\AxRule{{}\vdash\Gamma,A\parr B\parr C}
+
\NulRule{{}\vdash A,A\orth}
+
{| border="1" cellpadding="10" cellspacing="0"
\NulRule{{}\vdash B,B\orth}
+
|-
\NulRule{{}\vdash C,C\orth}
+
| '''Description'''
\TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth}
+
| '''Command'''
\LabelRule{\rulename{cut}}
+
| '''Example'''
\BinRule{{}\vdash\Gamma,A,B,C}
+
| '''LaTeX source'''
\UnaRule{{}\vdash\Gamma,A\parr B\parr C}
+
|-
\DisplayProof
+
| Axiom node <br /> (for hypotheses)
</math>
+
| <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\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\nlimp B
A\nlimp B
A\limpinv B
A\limpinv B
A\nlimpinv B
A\nlimpinv B
A\linequiv B
A\linequiv B
A\nlinequiv B
A\nlinequiv 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
A\pinj B
A\pinj B
\inner{A}{B}
\inner{A}{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
  \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
Personal tools