Typing:
propositional
symbol  type comment
∧/\
∨\/
¬!
FFF
TTT
UUU
→-->
↔<->
&&&&short-circuit and
||||short-circuit or
quantifiers
symboltype
∀ x:AA x:
∀ x; 0 ≤ x < y:     AA x; 0 <= x < y:
∃ x:EE x:
∃ x; x + 2 ≠ z: EE x; x+2 != z:

(Between ; and :, not all operators are available)
reasoning
symbol  type comment
⇒==>
⇐<==
⇔<=>unifies U and F
≡===does not unify U and F
subproofstarts a sub-reasoning
subendends a sub-reasoning
originalrefers to the first formula of the (sub-)reasoning
A global assumption (i.e., axiom) may be added to the front, e.g.: assume x > 3 \/ x = y;
arithmetic
symboltype
<<
≤<=
==
≠!=
≥>=
>>
++
−-
3y3y
y ⋅ 3y*3
|2x − 5||2x-5|
x + 1
6
(x+1)/6
2
3
4
2 3/4
(3 + 4)(x + 5)    (3+4)(x+5)


You may copy symbols from here: ≤ ≠ ≥ ¬ ∧ ∨ → ↔ ⇐ ⇒ ⇔ ≡ ∀ ∃

My CSEDU 2021 Publication Examples

This page contains the MathCheck examples in the publication “Automated Checking of Flexible Mathematical Reasoning in the Case of Systems of (In)Equations and the Absolute Value Operator” that appeared in the Proceedings of the 13th International Conference on Computer Supported Education - Volume 2: CSEDU, 324-331, 2021 (publisher's version). Feel free to try any or all of them!

“New tab” makes the feedback by MathCheck appear in a new browser tab or window, and “to the right” makes it appear in the box on the right. You may freely choose which one you click. You may also click both. Often it is a good idea to try “to the right” first, and if the feedback is so extensive that reading it from the box is inconvenient, then click “new tab”. Please try both now!

The introductory example in Figures 1 and 2.

or

You may change any input as much as you want, to see how MathCheck reacts. Please change any - to + in the above, and click “new tab” or “to the right”. Then try some changes of your own choice.

You can get all original inputs back by reloading this web page. In many browsers, it can be done with ⟨CTRL⟩-⟨F5⟩ or ⟨CTRL⟩-⟨SHIFT⟩-⟨R⟩ (press the two or three keys simultaneously).

Instructions for typing are found by moving the cursor to a brown area on the top right of the screen. It is also possible to copy and paste some non-keyboard symbols from below the box on the right.

One more trick: by putting the <=>, ==> or similar to the very beginning of the line, you can force a new line start in the feedback at that place. By putting just anything before it, for instance a space, this effect is cancelled. You may test this by adding a space to the beginning of the second line in the above answer box.

Here are the rest of the examples. Try any changes you want!

The incorrect input example in Figure 3.

or

The incompletely solved example in Figure 4.

or

The intervals of roots and division by zero example in Figure 5.

or

The unnecessarily complicated final answer example in Figure 6.

or

An example of the use of ∧ in Figure 7.

or

A clumsy solution to |a − 3| = 2a in Figure 8.

or

An incorrect implication whose converse is correct in Figure 9.

or

The lower box yields a different feedback from the paper. This is because I got the “Implication was used without returning to the original” feature working (in the paper it was work in progress). If that bothers you, then tick off the following and try again:

Solving Pólya’s problem in Figure 10.

or

Solving Pólya’s problem without subproofs.

or

Exploiting assume in a ==>- and <==-free solution by cases in Figure 11.

or

A solution by cases using <== instead of subproofs.

or

Using assume to deal with division by zero, avoiding ==> and <==.

or

The difference between → and ⇒. After trying, please remove the parentheses ( ) and try again.

or

Expression trees of the above. After trying, please remove the parentheses ( ) and try again.

or

Finally, there is one more thing I would like you to know. None of these examples needs the teacher tell anything to MathCheck. The teacher may give all these problems hand-written on paper, for instance.

To see that this is the case, copy any of the examples to the answer box below and try it there: you will get the same feedback as you got above. As a matter of fact, you may copy any example to any of the above answer boxes, and the feedback will match the example you copied there (and thus it may fail to match the caption above the answer box). (Well, if you tick off the checkbox above, then the corresponding answer box will be an exception; it then checks fewer things on the final answer. And also the expression tree boxes are different.)

Insist that the answer is explicit and simplified
or

(Addition 2022-01-04) Here is an example of a verbally stated problem where the student must first find the correct system of equations.

One hundred degrees Celsius is the same temperature as 212 degrees Fahrenheit. ‒40 degrees Celsius is the same temperature as ‒40 degrees Fahrenheit. The connection between these two temperature scales is of the form F = aC + b. Derive the values of the constants a and b by writing a system of equations and solving it.

tai