Recommendations
m (→Proofs: use of \rulename) |
(typo in url) |
||
(3 intermediate revisions by 2 users not shown) | |||
Line 48: | Line 48: | ||
=== 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{\rulename{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{\rulename{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 81: | Line 83: | ||
\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 87: | Line 89: | ||
\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 97: | Line 99: | ||
\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 103: | Line 105: | ||
\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 112: | Line 114: | ||
\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 118: | Line 120: | ||
\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 128: | Line 130: | ||
\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 134: | Line 136: | ||
\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>