Recommendations
From LLWiki
(Difference between revisions)
(→Proofs: \VdotsRule added) |
(typo in url) |
||
| (One intermediate revision by one user 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,B,C} |
+ | \AxRule{} |
| − | \VdotsRule{\pi}{{}\vdash\Gamma,A\parr B\parr C} |
+ | \VdotsRule{s}{{}\vdash\Gamma,A\imp B} |
| − | \NulRule{{}\vdash A,A\orth} |
+ | \AxRule{} |
| − | \NulRule{{}\vdash B,B\orth} |
+ | \VdotsRule{t}{{}\vdash\Gamma, A} |
| − | \NulRule{{}\vdash C,C\orth} |
+ | \BinRule{{}\vdash \Gamma, B} |
| − | \TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth} |
+ | \LabelRule{\rulename{modus ponens}} |
| − | \LabelRule{\rulename{cut}} |
+ | \DisplayProof |
| − | \BinRule{{}\vdash\Gamma,A,B,C} |
+ | \quad |
| − | \UnaRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \longrightarrow_\beta |
| + | \quad |
||
| + | \AxRule{} |
||
| + | \VdotsRule{s[t/x]}{{}\vdash\Gamma, B} |
||
\DisplayProof |
\DisplayProof |
||
</pre> |
</pre> |
||
<math> |
<math> |
||
| − | \AxRule{{}\vdash\Gamma,A,B,C} |
+ | \AxRule{} |
| − | \VdotsRule{\pi}{{}\vdash\Gamma,A\parr B\parr C} |
+ | \VdotsRule{s}{{}\vdash\Gamma,A\imp B} |
| − | \NulRule{{}\vdash A,A\orth} |
+ | \AxRule{} |
| − | \NulRule{{}\vdash B,B\orth} |
+ | \VdotsRule{t}{{}\vdash\Gamma, A} |
| − | \NulRule{{}\vdash C,C\orth} |
+ | \BinRule{{}\vdash \Gamma, B} |
| − | \TriRule{{}\vdash A,B,C,A\orth\tens B\orth\tens C\orth} |
+ | \LabelRule{\rulename{modus ponens}} |
| − | \LabelRule{\rulename{cut}} |
+ | \DisplayProof |
| − | \BinRule{{}\vdash\Gamma,A,B,C} |
+ | \quad |
| − | \UnaRule{{}\vdash\Gamma,A\parr B\parr C} |
+ | \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 === |
||
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
![\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](/mediawiki/images/math/2/b/8/2b8b9c1c37f91d8bb8bca92e696ed04b.png)
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>
