Recommendations

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (User account: typos)
(typo in url)
 
(4 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{\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 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

[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

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>


\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}_2}
\BinRule{\textit{Concl}}
\DisplayProof



\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

Personal tools