Proof Syntax
proof: a group of lines separated onto vertically adjacent lines. An empty line will be
understood as the end of the proof constituted by preceding, non-empty lines.
line:: [line_number ]sentence justification prior_lines
line_number: line numbers are not necessary, as the back-end parser will identify the line by position, but
are helpful when writing the proof. The following space is necessary if line numbers and attending
punctuation are present. No spaces among line number and punctuation (e.g.
'1. ', '2 ', '3$$$ '). First character must be a number.
sentence: Alphabetical characters and logical operators organized by parentheses; no spaces are allowed within a sentence. Sentence
letters are one alphabetical character. Case matters: a!=A. Accepted
logical operators appear on the buttons below the line form. A sentence can have only one general
operator--a logical operator that binds the entire sentence and is not bound by parentheses. All complex operands, i.e. operands that
contain logical operators, must be encapsulated in parentheses. Simple operands--sentence
letters--must not occur within parentheses:
parentheses->operator
~operator
~parentheses MT 1,2
justification: any one of the logical rules listed in the dropdown menu. Must either be the
full name or the abbreviation shown in the rule information or added by the line form.
Capitalization is optional, omit spaces and punctuation (e.g. demorganstheorems).
prior_lines: 0-3 numbers delimited with commas or a dash. If cited individually, separate
numbers with a comma. A dash is used
when citing a range. See rule information under the line form for rule-specific constraints. No spaces.