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 `;`.
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 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 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...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_help	Print short typing instructions.
CFG_compare	Compare the context-free 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 context-free grammar for future tasks.
CFG_set2	Set the latter context-free 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 non-terminal is used.)
CFG_start2	Set the start symbol for the grammar given by `CFG_set2`. (By default, the first non-terminal 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 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.
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 odd-looking 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 “model-solution” 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.