MathCheck Instructions

This document is as of 2021-11-16. It lacks all more recent features of MathCheck.

In ready-made 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 double-precision 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 ;.
originalRefers 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.
subendEnds a subproof.
subproofStarts 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 non-numeric 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 xMake the variable of array index type.
integer xMake the variable of integer type.
prime pMake the variable of prime number type.
real kMake 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.

arithmeticSelect the arithmetic mode. Checks a chain of arithmetic expressions separated by <, ≤, =, >, and ≥.
array_claim A[0...n-1]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_helpPrint short typing instructions.
CFG_compareCompare the context-free grammars given by the CFG_set and CFG_set2 commands.
CFG_inTest whether the string given next is in the language specified earlier by CFG_set.
CFG_longSet an upper bound to the length of answer strings.
CFG_not_inThis one is opposite to CFG_in.
CFG_setSet a context-free grammar for future tasks.
CFG_set2Set the latter context-free grammar for CFG_cmp.
CFG_shortSet a lower bound to the length of answer strings.
CFG_startSet the start symbol for the grammar given by CFG_set. (By default, the first non-terminal is used.)
CFG_start2Set the start symbol for the grammar given by CFG_set2. (By default, the first non-terminal is used.)
CFG_treeDraw 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 teacher-given 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 teacher-given roots. The roots must certainly satisfy the assumption despite rounding errors.
helpPrint this file.
mathcheckPrint 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_treeDraw the expression tree of an expression, etc. This command makes fewer sanity checks than usual.
presburgerSelect the natural number logic mode. Checks a reasoning chain in the logic.
prop_logicSelect the propositional logic mode without the undefined truth value. Checks a reasoning chain in the logic.
prop3_logicSelect the propositional logic mode with the undefined truth value. Checks a reasoning chain in the logic.
real_logicSelect 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_compThe 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 48If the final expression yields at most 48 nodes, a bonus statement is printed.
ban_compThe relation chain must not contain <, ≤, >, and ≥ or ⇐ and ⇒.
end_of_answerIf 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 odd-looking error messages. It should be used in the beginning of the next question. If followed by !, stops reading input.
f_allow_UThe 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_CNFThe final expression must be in conjunctional normal form or a product of sums.
f_DNFThe final expression must be in disjunctional normal form or a sum of products.
f_nodes 56The 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_rangeIn 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 sqrtThe final expression must contain √.
f_simplifyThe final expression must be simplified. This command does not yet work very well.
f_top_opr sqrtThe 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_exprPrint “model-solution” instead of the next expression.
solve xThe final expression must be solved with respect to x.
solve_allThe final expression must be solved with respect to all variables.
var4Allow four variables in the arithmetic mode, at the cost of less careful testing of the expressions. (By default, three are allowed.)
var5Allow 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_onWarn about ambiguous grammar.
CFG_CR_onIgnore newlines in strings, to facilitate combining CFG items from more than one HTML textarea.
debug_onMake MathCheck print mysterious additional information.
draw_offDo not draw the graphs of both sides when a relation fails. Do not draw the teacher's expression tree.
exam_onDo not give feedback on semantics.
fail_textPrint 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_textPrint 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_onDo 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_offDo not attempt to prove relations, etc.
resetReset most global settings (not debug nor exam).
verbose_onPrint headers, etc., in the feedback.

Deprecated or Removed Commands

#DNo longer exists. Use DD instead.
#xxxNo longer exists. Use xxx instead. #(, #), #*, and #/ are not deprecated.
f_ban_derBans the use of derivatives in the final formula. Use f_ban DD; instead.
forget_errorsShow the link to the next problem page even if the solution contains errors. Chained problem pages proved not so good.
funcpar_onNo longer exists. Alternative rules for the parentheses cause confusion. Use #( and #) when necessary.
lfNo longer exists. Use /**/ instead.
newproblemNo 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_URLIf 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_onUse the undefined truth value also in the propositional logic mode. Use Prop3_logic instead.
skip_errorIf possible, continue checking even if there is an error. Technically problematic and not very necessary.
undef_offThis is pedagogically unwise, use the assume mechanism.