Recommendations
(→Definitions and theorems: Remark added) |
(typo in url) |
||
(6 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
== User account == |
== User account == |
||
− | * use "FirstName LastName" as Username |
+ | * Use "FirstName LastName" as Username. |
− | * use a valid e-mail address |
+ | * Use a valid e-mail address. |
+ | |||
+ | == Conventions == |
||
+ | |||
+ | * Use English only, even for comments, discussions, ... |
||
+ | * Use <tt><nowiki>== Header ==</nowiki></tt> for higher-level headers, ''do not'' use only one equals sign on a side. |
||
== Notations == |
== Notations == |
||
Line 43: | Line 43: | ||
=== Proofs === |
=== Proofs === |
||
− | The syntax for proofs is based on the [http://whttp://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/ bussproofs.sty] package. The only allowed macros are those used in the following example: |
+ | The syntax for proofs is based on the [http://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/ bussproofs.sty] package, but available only through a sugar-coated specific to llwiki. Here is an example: |
− | |||
<pre> |
<pre> |
||
− | \AxRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \AxRule{} |
− | \NulRule{{}\vdash A,A\orth} |
+ | \VdotsRule{s}{{}\vdash\Gamma,A\imp B} |
− | \NulRule{{}\vdash B,B\orth} |
+ | \AxRule{} |
− | \NulRule{{}\vdash C,C\orth} |
+ | \VdotsRule{t}{{}\vdash\Gamma, A} |
− | \TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth} |
+ | \BinRule{{}\vdash \Gamma, B} |
− | \LabelRule{\textit{cut}} |
+ | \LabelRule{\rulename{modus ponens}} |
− | \BinRule{{}\vdash\Gamma,A,B,C} |
+ | \DisplayProof |
− | \UnaRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \quad |
+ | \longrightarrow_\beta |
||
+ | \quad |
||
+ | \AxRule{} |
||
+ | \VdotsRule{s[t/x]}{{}\vdash\Gamma, B} |
||
\DisplayProof |
\DisplayProof |
||
</pre> |
</pre> |
||
<math> |
<math> |
||
− | \AxRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \AxRule{} |
− | \NulRule{{}\vdash A,A\orth} |
+ | \VdotsRule{s}{{}\vdash\Gamma,A\imp B} |
− | \NulRule{{}\vdash B,B\orth} |
+ | \AxRule{} |
− | \NulRule{{}\vdash C,C\orth} |
+ | \VdotsRule{t}{{}\vdash\Gamma, A} |
− | \TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth} |
+ | \BinRule{{}\vdash \Gamma, B} |
− | \LabelRule{\textit{cut}} |
+ | \LabelRule{\rulename{modus ponens}} |
− | \BinRule{{}\vdash\Gamma,A,B,C} |
+ | \DisplayProof |
− | \UnaRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \quad |
+ | \longrightarrow_\beta |
||
+ | \quad |
||
+ | \AxRule{} |
||
+ | \VdotsRule{s[t/x]}{{}\vdash\Gamma, B} |
||
\DisplayProof |
\DisplayProof |
||
</math> |
</math> |
||
+ | |||
+ | A list of all available macros for proofs is available on the page for the [[LLWiki_LaTeX_Style#Proof_trees|LLWiki LaTeX package]]. |
||
=== Set of rules === |
=== Set of rules === |
||
Line 76: | Line 78: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_1} |
+ | \LabelRule{\rulename{Rule}_1} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 82: | Line 84: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_1} |
+ | \LabelRule{\rulename{Rule}_1} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 92: | Line 94: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_3} |
+ | \LabelRule{\rulename{Rule}_3} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 98: | Line 100: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_4} |
+ | \LabelRule{\rulename{Rule}_4} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 107: | Line 109: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_1} |
+ | \LabelRule{\rulename{Rule}_1} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 113: | Line 115: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_2} |
+ | \LabelRule{\rulename{Rule}_2} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 123: | Line 125: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_3} |
+ | \LabelRule{\rulename{Rule}_3} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
||
Line 129: | Line 131: | ||
\AxRule{\textit{Hyp}_1} |
\AxRule{\textit{Hyp}_1} |
||
\AxRule{\textit{Hyp}_2} |
\AxRule{\textit{Hyp}_2} |
||
− | \LabelRule{\text{Rule}_4} |
+ | \LabelRule{\rulename{Rule}_4} |
\BinRule{\textit{Concl}} |
\BinRule{\textit{Concl}} |
||
\DisplayProof |
\DisplayProof |
Latest revision as of 15:06, 8 December 2009
Contents |
[edit] User account
- Use "FirstName LastName" as Username.
- Use a valid e-mail address.
[edit] Conventions
- Use English only, even for comments, discussions, ...
- Use == Header == for higher-level headers, do not use only one equals sign on a side.
[edit] Notations
For uniformity, use the common notations when they are already defined, and add your notations to the notations page when you introduce new ones.
[edit] Definitions and theorems
For theorem-style environments, use the appropriate predefined templates: Definition, Theorem, Proposition, Lemma, Corollary (with an optional parameter "title"). Additional templates are Proof for proofs and Remark for remarks.
{{Definition|title=Concept|A new concept.}} {{Theorem|This is a nice concept.}} {{Proof|Left to the reader.}} {{Remark|Really nice, isn't it?}} |
Definition (Concept) A new concept. Theorem This is a nice concept. Proof. Left to the reader. Remark: Really nice, isn't it?
|
[edit] Mathematical typesetting
[edit] Formulas
- use the macros defined in the LLWiki LaTeX Style
[edit] Proofs
The syntax for proofs is based on the bussproofs.sty package, but available only through a sugar-coated specific to llwiki. Here is an example:
\AxRule{} \VdotsRule{s}{{}\vdash\Gamma,A\imp B} \AxRule{} \VdotsRule{t}{{}\vdash\Gamma, A} \BinRule{{}\vdash \Gamma, B} \LabelRule{\rulename{modus ponens}} \DisplayProof \quad \longrightarrow_\beta \quad \AxRule{} \VdotsRule{s[t/x]}{{}\vdash\Gamma, B} \DisplayProof
A list of all available macros for proofs is available on the page for the LLWiki LaTeX package.
[edit] Set of rules
For a group of rules, separate rules on a line by \qquad and separate lines by <br />.
<math> \AxRule{\textit{Hyp}_1} \AxRule{\textit{Hyp}_2} \LabelRule{\rulename{Rule}_1} \BinRule{\textit{Concl}} \DisplayProof \qquad \AxRule{\textit{Hyp}_1} \AxRule{\textit{Hyp}_2} \LabelRule{\rulename{Rule}_1} \BinRule{\textit{Concl}} \DisplayProof </math> <br /> <math> \AxRule{\textit{Hyp}_1} \AxRule{\textit{Hyp}_2} \LabelRule{\rulename{Rule}_3} \BinRule{\textit{Concl}} \DisplayProof \qquad \AxRule{\textit{Hyp}_1} \AxRule{\textit{Hyp}_2} \LabelRule{\rulename{Rule}_4} \BinRule{\textit{Concl}} \DisplayProof </math>