LLWiki LaTeX Style - Revision history

Olivier Laurent: /* Proof trees */ typo

2013-06-27T13:51:18Z

‎Proof trees: typo

Olivier Laurent: /* Mathematical notations */ Added \ping, \inner, \Inner (used for proof-nets)

2012-08-31T15:13:52Z

‎Mathematical notations: Added \ping, \inner, \Inner (used for proof-nets)

Olivier Laurent: /* Mathematical notations */ added: limpinv, nlimp, nlimpinv, nlinequiv

2010-04-21T13:41:32Z

‎Mathematical notations: added: limpinv, nlimp, nlimpinv, nlinequiv

Lionel Vaux: /* Proof trees */ describe all available commands for proof trees

2009-07-06T15:58:29Z

‎Proof trees: describe all available commands for proof trees

Olivier Laurent: /* Proof trees */ \VdotsRule added

2009-06-10T17:24:17Z

‎Proof trees: \VdotsRule added

Olivier Laurent: /* Mathematical notations */ \powerset,... added

2009-06-10T17:23:08Z

‎Mathematical notations: \powerset,... added

Lionel Vaux: example of proof tree

2009-06-10T09:39:26Z

example of proof tree

Olivier Laurent: /* Mathematical notations */ \Bot and \Perp added

2009-02-08T14:30:36Z

‎Mathematical notations: \Bot and \Perp added

Olivier Laurent: /* Mathematical notations */ \biorth and \triorth added

2009-02-08T14:12:34Z

‎Mathematical notations: \biorth and \triorth added

Olivier Laurent: /* Mathematical notations */ \linequiv and \set added

2009-01-21T20:07:57Z

‎Mathematical notations: \linequiv and \set added

← Older revision		Revision as of 13:51, 27 June 2013
Line 223:		Line 223:
	\DisplayProof</pre>		\DisplayProof</pre>
	\|}		\|}
−	<math>

@@ Line 116: / Line 116: @@
 | <math>A\Perp B</math>
 | <pre>A\Perp B</pre>
 |-
 |}

@@ Line 44: / Line 44: @@
 | <math>A\limp B</math>
 | <pre>A\limp B</pre>
 |-
 | <math>A\linequiv B</math>
 | <pre>A\linequiv B</pre>
 |-
 | <math>\shpos A</math>

← Older revision		Revision as of 15:58, 6 July 2009
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>

@@ Line 110: / Line 110: @@
 <math>
-\AxRule{{}\vdash\Gamma,A\parr B\parr C}
+\AxRule{{}\vdash\Gamma,A,B,C}
 \NulRule{{}\vdash A,A\orth}
 \NulRule{{}\vdash B,B\orth}

@@ Line 86: / Line 86: @@
 | <math>\set{x}{P}</math>
 | <pre>\set{x}{P}</pre>
 |-
 | <math>\Bot</math>

← Older revision		Revision as of 09:39, 10 June 2009
Line 94:		Line 94:
	\|-		\|-
	\|}		\|}
		+
		+	== Proof trees ==
		+
		+	<math>
		+	\AxRule{{}\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>

@@ Line 5: / Line 5: @@
 | <math>A\orth</math>
 | <pre>A\orth</pre>
 |-
 | <math>A\tens B</math>

@@ Line 38: / Line 38: @@
 | <math>A\limp B</math>
 | <pre>A\limp B</pre>
 |-
 | <math>\shpos A</math>
@@ Line 74: / Line 77: @@
 | <math>A\cliq B</math>
 | <pre>A\cliq B</pre>
 |-
 |}