MathCheck Instructions
This document is as of 20211116.
It lacks all more recent features of MathCheck.
In readymade problems, the use of commands may have been
restricted to those relevant for the problem.
There are two mechanisms towards this aim.
If the textarea has the name “exam”, then many commands are unavailable.
Commands may also be banned by some commands mentioned below.
Arithmetic and Parentheses
`54321`  54321 
`frac(54)(321)`  54/321 
`54 frac(3)(21)`  54 3/21 
`54.321`  54.321 
`pi`  pi 
`e`  e 

`+`  + 
`−`   
`*`  * 
`x/y`  x/y 
`frac(x+1)(2y)`  (x+1)/(2y) #/(x+1)(2y) 
`x^y`  x^y 
`x^(y z)`  x^(y z) 

`(`  ( 
`)`  ) 
`(`  #( 
`)`  #) 
`[`  [ 
`]`  ] 
`\ text(div)\ `  div 
`mod`  mod 
`n!`  n! 

`sqrt x+1`  sqrt x+1 
`sqrt(x+1)`  sqrt(x+1) 
`root(n)(x+1)`  root(n)(x+1) 
`x+1`  x+1 abs(x+1) 
`__x+1__`  _x+1_ floor(x+1) 
`~x+1~`  ^x+1^ ceil(x+1) 
`d/(d x) sin 5x`  DD x sin 5x 

`sin`  sin 
`cos`  cos 
`tan`  tan 
`cot`  cot 
`ln`  ln 
`log`  log 
`log_2`  log2 
`sinh`  sinh 
`cosh`  cosh 
`tanh`  tanh 

The input symbols ( and ) denote
ordinary parentheses and #( and #) denote hard
parentheses.
MathCheck removes unnecessary ordinary parentheses, but always prints hard
parentheses even if they are unnecessary.
A, …, Z, a, …, z, and the Greek
letters listed below can be used as variables, excluding e and π.
If the problem mode assumes ordinary numbers, then I, …, N and
i, …, n hold integer and others hold real values, unless the
teacher has specified otherwise.
MathCheck is not good in finding errors if the floor or
ceiling function is used.
MathCheck uses precise rational number arithmetic when it can
and then reverts to intervals of doubleprecision values.
Also decimal number tokens yield rational values, whenever possible.
The functions ddn and dup return the lower and upper
bound of the interval.
Comparisons and Logic
`<=`  <= 
`<`  < 
`=`  = 
`!=`  != 
`>=`  >= 
`>`  > 

`not`  ! not 
`^^`  /\ and ^^ 
`vv`  \/ or vv 
`rarr`  > 
`harr`  <> 
`sf"F"`  FF 
`sf"U"`  UU 
`sf"T"`  TT 

`\ sf"&&"\ `  && 
`\ sf""\ `   
`>>`  >> 
`**`  * 
`AA x:`  AA x: 
`AA i; 1 <= i <= n:`  AA i; 1 <= i <= n: 
`EE x:`  EE x: 
`EE i; 1 <= i <= n:`  EE i; 1 <= i <= n: 

`rArr`  ==> 
`lArr`  <== 
`hArr`  <=> 
`=`  === 

Reasoning Chains
A reasoning chain may contain ⇐, ⇔, ⇒ and ≡, and the following:
assume x != 1 /\ y >= x;  Set a condition
that is assumed to hold throughout the (sub)proof. One may use enda
instead of ;. 
original  Refers to the first formula in a
reasoning chain. If original is the first formula of a subproof,
then it refers to the first formula of the parent proof. 
subend  Ends a subproof. 
subproof  Starts a subproof. 
What formulas in a reasoning chain may contain depends on the problem mode.
Typically most logical and comparison operators are allowed, but only a small
set of arithmetic operators.
Variables are automatically of the type needed by the problem mode.
Greek Letters
`alpha`  al 
`beta`  be 
`gamma`  ga 
`delta`  de 
`varepsilon`  ve 
`epsilon`  ep 
`zeta`  ze 

`eta`  et 
`theta`  th 
`vartheta`  vt 
`iota`  io 
`kappa`  ka 
`lambda`  la 
`mu`  mu 

`nu`  nu 
`xi`  xi 
`rho`  rh 
`sigma`  si 
`tau`  ta 
`upsilon`  up 

`phi`  ph 
`varphi`  vp 
`chi`  ch 
`psi`  ps 
`omega`  om 

`Gamma`  Ga GA 
`Delta`  De DE 
`Theta`  Th TH 
`Lambda`  La LA 
`Xi`  Xi XI 

`Pi`  Pi PI 
`Sigma`  Si SI 
`Phi`  Ph PH 
`Psi`  Ps PS 
`Omega`  Om OM 

Lexical Rules
Spaces and newlines may be freely used between tokens.
If a nonnumeric token ends and the next one starts with a letter or digit,
there must be at least one space or newline in between.
These symbols can also be given as Unicode characters:
¬ ² ³ Γ Δ Θ Λ Ξ Π Σ Φ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω ϑ ϕ ϵ
← → ↔ ↠ ⇐ ⇒ ⇔ ∀ ∃ − √ ∧ ∨ ≠ ≡ ≤ ≥ ⋅ ⌈ ⌉ ⌊ ⌋
Special Commands
/**/  Start a new line. A new line may also
be started by putting the ⇔, ⇒, etc., to the very beginning of the line. In
problem modes that do not support them, put =, >, etc., to the very
beginning of the line. 
/* two to the `n` is `2^n` */  Write a
comment and start a new line. Passages surrounded by grave accent characters
will be shown as mathematics. 
assume x != 1 /\ y^2 < sin x;  Restrict
the range of variables. Any comparisons and propositional operators may be used
in the condition. One may use enda instead of ;. Works in
the arithmetic and draw function modes, and almost all problem modes that
support logical reasoning chains. Unless otherwise stated, this must be next to
the problem mode keyword. 
index x  Make the variable of array index
type. 
integer x  Make the variable of integer
type. 
prime p  Make the variable of prime number
type. 
real k  Make the variable of real number
type. 
Problem Modes and Related
The versions with capital initial letter do and with small
case do not reset most global settings.
arithmetic  Select the arithmetic mode.
Checks a chain of arithmetic expressions separated by <, ≤, =, >, and
≥. 
array_claim A[0...n1]  Select the array
claim mode. Checks a chain of predicates on A separated by ⇔ or ≡. The
index lower bound must be an integer. The upper bound must be a variable with
an optional + or − integer. Does not show the first claim explicitly. Testing
is based on trying all small arrays whose elements are in a small range of
integers. The smallest tested value is by default 0, but can be set with
array_test_min. 
brief_help  Print short typing
instructions. 
CFG_compare  Compare the contextfree
grammars given by the CFG_set and CFG_set2
commands. 
CFG_in  Test whether the string given next
is in the language specified earlier by CFG_set. 
CFG_long  Set an upper bound to the length
of answer strings. 
CFG_not_in  This one is opposite to
CFG_in. 
CFG_set  Set a contextfree grammar for
future tasks. 
CFG_set2  Set the latter contextfree
grammar for CFG_cmp. 
CFG_short  Set a lower bound to the length
of answer strings. 
CFG_start  Set the start symbol for the
grammar given by CFG_set. (By default, the first nonterminal is
used.) 
CFG_start2  Set the start symbol for the
grammar given by CFG_set2. (By default, the first nonterminal is
used.) 
CFG_tree  Draw the parse tree of the string
given next according to the grammar given by CFG_set, or report that
it is not in its language. 
draw_function 10 10 5 5; x^2; 1/x; sin x  Draw graphs of at most six functions. The numbers are the extreme
coordinates: left right bottom top, and they are optional starting from the
last. 
equation x=3 \/ x=1; x^2  2x  3 = 0 <=>  Select the equation mode. In the solution, also ⇒ may be used, but
then there must be original ⇔ later on. The teachergiven roots may
also be x FF, to indicate that there are no roots; or x,
to not give the roots (this last feature does not yet work well). One may use
ends instead of ;. The assume clause, if given, must be
next to the teachergiven roots. The roots must certainly satisfy the
assumption despite rounding errors. 
help  Print this file. 
mathcheck  Print copyright information. The
resetting version is written as MathCheck. 
modulo 17 TT <=> EE x: x^2 = 1  Select the modulo mode. Checks a reasoning chain in modular
arithmetic. The number must be between 2 and 25 inclusive. 
expression_tree  Draw the expression tree of
an expression, etc. This command makes fewer sanity checks than
usual. 
presburger  Select the natural number logic
mode. Checks a reasoning chain in the logic. 
prop_logic  Select the propositional logic
mode without the undefined truth value. Checks a reasoning chain in the
logic. 
prop3_logic  Select the propositional logic
mode with the undefined truth value. Checks a reasoning chain in the
logic. 
real_logic  Select the real number logic
mode. Checks a reasoning chain in the logic. 
tree_compare 1(2+3);  Select the expression
tree comparison mode. Checks that the expressions have the same expression
trees. Does not show the first expression explicitly. 
Local Settings and Related
Local settings only affect the current problem.
#*  This can be used to denote invisible
multiplication as a top or banned operator. 
allow_comp  The relation chain may contain
<, ≤, >, and ≥ or ⇐ and ⇒. This command is needed to cancel their
automatic ban in exam textareas, solve x, solve_all, etc.. 
b_nodes 48  If the final expression yields
at most 48 nodes, a bonus statement is printed. 
ban_comp  The relation chain must not
contain <, ≤, >, and ≥ or ⇐ and ⇒. 
end_of_answer  If answers to two or more
problems are submitted at the same time, this prevents the next question from
being interpreted as part of the previous answer. It thus prevents oddlooking
error messages. It should be used in the beginning of the next question. If
followed by !, stops reading input. 
f_allow_U  The undefined truth value is by
default not allowed in the final answer, but may be allowed with
f_allow_U. This currently only works in the array claim
mode. 
f_ban ^ sqrt root;  The final expression
must not contain the listed operators. When banning *, it may make
sense to also ban #*, and vice versa. 
f_CNF  The final expression must be in
conjunctional normal form or a product of sums. 
f_DNF  The final expression must be in
disjunctional normal form or a sum of products. 
f_nodes 56  The final expression must not
yield more than 56 expression tree nodes. 
f_polynomial x;  The final expression must
be in polynomial form with respect to x / all variables. The variable may be
omitted. 
f_range  In modular arithmetic mode, the
final expression must not contain constants outside the range 0, …, modulus
minus 1. 
f_rational x;  The final expression must be
in rational or polynomial form with respect to x / all variables. The variable
may be omitted. 
f_req_opr sqrt  The final expression must
contain √. 
f_simplify  The final expression must be
simplified. This command does not yet work very well. 
f_top_opr sqrt  The top operator of the
final expression must be √. If the operator is `frac(d)(d ...)`, ∀, or ∃, also
the variable must be given. The operator (independently of the variable) may
not occur elsewhere in the expression. When using * as the operator,
it may make sense to ban #*, and vice versa. 
hide_expr  Print “modelsolution” instead of
the next expression. 
solve x  The final expression must be solved
with respect to x. 
solve_all  The final expression must be
solved with respect to all variables. 
var4  Allow four variables in the arithmetic
mode, at the cost of less careful testing of the expressions. (By default,
three are allowed.) 
var5  Allow five variables in the arithmetic
mode, at the cost of less careful testing of the expressions. (By default,
three are allowed.) 
Global Settings and Related
Global settings are not automatically reset for each new
problem.
The effect of each xxx_off can be cancelled with xxx_on
and vice versa.
CFG_ambiguous_on  Warn about ambiguous
grammar. 
CFG_CR_on  Ignore newlines in strings, to
facilitate combining CFG items from more than one HTML textarea. 
debug_on  Make MathCheck print mysterious
additional information. 
draw_off  Do not draw the graphs of both
sides when a relation fails. Do not draw the teacher's expression
tree. 
exam_on  Do not give feedback on
semantics. 
fail_text  Print the text following this
command for each mathematically incorrect answer. The text ends at the next
empty line, and # acts as the escape character facilitating writing
HTML. 
ok_text  Print the text following this
command for each correct answer. The text ends at the next empty line, and
# acts as the escape character facilitating writing HTML. 
only_no_yes_on  Do not print the information
whose purpose is to help the student find the error. This is useful, for
instance, if the correct answer is a number. 
prove_off  Do not attempt to prove
relations, etc. 
reset  Reset most global settings (not debug
nor exam). 
verbose_on  Print headers, etc., in the
feedback. 
Deprecated or Removed Commands
#D  No longer exists. Use DD
instead. 
#xxx  No longer exists. Use xxx
instead. #(, #), #*, and #/ are not
deprecated. 
f_ban_der  Bans the use of derivatives in
the final formula. Use f_ban DD; instead. 
forget_errors  Show the link to the next
problem page even if the solution contains errors. Chained problem pages proved
not so good. 
funcpar_on  No longer exists. Alternative
rules for the parentheses cause confusion. Use #( and #)
when necessary. 
lf  No longer exists. Use /**/
instead. 
newproblem  No longer exists. Use
arithmetic, prop_logic, etc., instead. 
next_URL https://...  If the answer is
correct, give the URL of the next problem page in the feedback. Chained problem
pages proved not so good. 
no_next_URL  If the answer is correct, tell
that this was the last problem in the series. Chained problem pages proved not
so good. 
parse_tree  “Parse” refers to a wrong thing.
Use expression_tree instead. 
prop3_on  Use the undefined truth value also
in the propositional logic mode. Use Prop3_logic instead. 
skip_error  If possible, continue checking
even if there is an error. Technically problematic and not very
necessary. 
undef_off  This is pedagogically unwise, use
the assume mechanism. 