Typing instructions:
arithmetic
symbolwrite
++
−-
3y3y
y ⋅ 3y*3
(3 + 4)(x + 5)(3+4)(x+5)
x + 1
y + 6
 (x+1)/(y+6) 
2
3
4
2 3/4
|x + 1||x+1|
x2nx^(2n)
√x + 1sqrt x+1
n√x + 1root(n)(x+1)

What symbols are available depends on the context.
There are also others: ln, log2, sin, div, etc.
comparisons
symbol write
<<
≤<=
==
≠!=
≥>=
>>
basic logic
symbol  write  remark
∧/\and (also and works)
∨\/or (also or works)
¬!not (also not works)
FFFfalse
TTTtrue
UUUundefined
→-->material implication
↔<->material equivalence
&&&&short-circuit and
||||short-circuit or
reasoning
symbol  write  remark
⇒==>
⇐<==
⇔<=>treats U and F as equivalent
≡===treats U and F as different

A subproof occurs between subproof and subend. The first formula of a (sub)proof can be referred to as original. At the very beginning of a subproof, original refers to the first formula on the previous level. A (sub)proof can be made to trust on an assumption by preceding it with assume formula ;.
quantifiers
symbolwrite
∀ x:AA x:
∀ x; 0 ≤ x < y:     AA x; 0 <= x < y:
∃ x:EE x:
∃ x; x + 2 ≠ z: EE x; x+2 != z:

The syntax of the part between ; and : has been restricted.

Logic Problem Examples

arithmetic feedback • line segment • cottage • minimum • Pólya’s problem • 3|x| ≥ |x − 3| + 5 • Selection Sort • volleyball • divisible by 7 • sum of cubes • ∃ P ∧ Q(x) • ∀ x: P(x) ∨ Q(x) • print a DFA

Just One Example of a Non-Logic Problem

Click either button to see the feedback by MathCheck.

or

Logic Problems on Real Numbers

For each of the following images, write a formula so that the formula is true if and only if x is in the blue area.

an image on the x-axis

or

an image on the x-axis

or

Write a short formula so that the formula is true if and only if x is in the blue area. HintSay within your answer that x is not 5.

an image on the x-axis

or

Write a formula that represents the green area. All points on the borderlines between white and green are green. You may first design and check each part of the cottage in the answer boxes that are further below.
a green cottage on x-y-coordinates

or

Here you may design each part of the cottage. The answers are not mathematically unique, because parts may overlap. For instance, the chimney may continue through the roof so that its lower end can be horizontal. However, only the most natural options are allowed for the window and roof (but, as is usual, they may be expressed in many mathematically equivalent ways).

Wall

or

Window (the formula should represent the white area inside the green area)

or

Chimney

or

Roof

or

Write a formula that says that x is one or the other of the numbers a and b. Hintx equals a or x equals b.

or

Write a formula that says that x is at most as big as both of a and b. Hintx is less than or equal to a and x is less than or equal to b.

or

Without using min or max, write a formula that says that x is the minimum of a and b. It suffices to solve the problem with a permissive maximum length, but if you want to become an expert, then solve it also with the difficult maximum length. If you want, you may leave a mathematically correct but too long formula in the answer box and continue by writing <=> and a new formula. Hint 1Combine your answers to the previous questions. Hint 2Add the parentheses “(” and “)” so that “x is one or the other of the numbers a and b” stays as an unbroken entity.
Permissive maximum length
Difficult maximum length

or

The above question was implemented in the real logic mode, because it is discussed in a section about that mode. That mode currently lacks the min and max operators. Here it is implemented in the integer logic mode, using min in the model answer and leaving it visible in the feedback. The teacher has told MathCheck not to accept min and max in the final answer.
Permissive maximum length
Difficult maximum length

or

The upper box contains a system of linear equations from George Pólya’s “How to Solve It”. Its contents cannot be changed. The lower box contains a MathCheck-checkable solution. It can be changed.
or

Solve the inequation 3|x| ≥ |x − 3| + 5. Start with ⇒, ⇐, ⇔, ≡, or subproof.

or

Problems on (At Least) Integer Artithmetic

Here is a C++ implementation of Selection Sort. Let n = A.size().

1 void SelectionSort( array_type & A ){
2   for( unsigned i = 0; i+1 < A.size(); ++i ){
3    unsigned p = i;
4     for( unsigned j = i+1; j < A.size(); ++j ){
5       if( A[j].x < A[p].x ){ p = j; }
6    }
7     elem_type tmp = A[i]; A[i] = A[p]; A[p] = tmp;
8  }
9}

What is known on the value of i in the beginning of line 3?

or

What is known on the values of i, j and p in the beginning of line 5?

or

What is known on the values of i and p in the beginning of line 7?

or

A volleyball set ends when a team has at least 25 points and at least 2 points more than the opposite team has. For instance, the points cannot be 35–28 but can be 15–8. Points are earned one at a time. Assume that the variables p hold q the numbers of points of the two teams.

Write a formula that says that the points can be p and q. You may choose yourself the kind of numbers that your formula talks about, and how short you try to make your answer. “Difficult maximum length” probably requires an inelegant formula.

maximum length natural numbers  integers   real numbers 
no limit 
middle difficulty 
difficult 


or

Without using the symbols div and mod, write a formula that says that n is divisible by 7! Hint 1Say that n may be obtained by multiplying some integer by seven. Hint 2Say that there is an integer such that when it is multiplied by 7, the result equals n.

or

Our next goal is to find the smallest natural number that can be written as a sum of two cubes of natural numbers in two different ways, and to find those two ways. The formula C(x, y) has been pre-programmed so that, to the extent needed below, it is true if and only if y = x3 ≥ 0. Please use it for representing cubes. You may write other expressions in the places of x and y. (For reasons that are related to fundamental limitations of computation, the integer logic mode of MathCheck does not accept x3 or x ⋅ x ⋅ x as such.)

Write a formula that says that x is the sum of the cubes of n and m.

or

Copy your previous answer to the box below. Doing so makes it possible to write S(n, m, x) to represent it further below. Also other expressions can be used in the place of n, m and x.

To find the numbers, we will misuse MathCheck. Write below a formula saying that x cannot be represented as the sum of two cubes in two different ways, where the sums of two cubes are n3 + m3 and k3 + h3. Use S(…, …, …) in your formula.

If your formula says the right thing, MathCheck sees it as an incorrect claim and gives a counter-example. The counter-example contains the numbers that we want to find. (This trick does not always yield the smallest counter-example, but in the case of this problem it does.) If your formula says something else, MathCheck will not give a counter-example, or gives a counter-example that does not tell the right numbers.

When you get the numbers, write them (except x) to the boxes further below, to test whether they are the right ones.

or

Write n, m, k and h.
or

Find also another natural number that can be represented as a sum of two cubes of natural numbers in two different ways. HintChange the previous formula so that the original counter-example no longer is a counter-example.
Write n, m, k and h.
or

In the next questions, P represents any formula where x does not occure free, and Q(x) represents any formula. It is possible that there is no shorter correct answer than the given formula as such.

Although MathCheck can deal with formulas, it cannot deal with symbols that represent arbitrary formulas. Therefore, when MathCheck checks your answer in the boxes below, it uses hidden formulas that depend on the value of the variable q so that all relevant possibilities will be tested. If you get a counter-example, please pay attention to the “left” and “right” values in it, and not to the values of q and x.

Write as short formulas as possible that mean the same as the given formulas, when P ≡ F.

P ∧ Q(x) ≡     or   
∃ x: P ∧ Q(x) ≡     or   
P ∧ ∃ x: Q(x) ≡     or   

Write as short formulas as possible that mean the same as the given formulas, when P ≡ T.

P ∧ Q(x) ≡     or   
∃ x: P ∧ Q(x) ≡     or   
P ∧ ∃ x: Q(x) ≡     or   

The results show that a certain law is valid. What law? AnswerLet P and Q(x) be formulas. If x does not occur free in P, then
∃ x: P ∧ Q(x)  ⇔  P ∧ ∃ x: Q(x)

Write such formulas P(x) and Q(x) on integers that the logical equivalence in the lowestmost box does not hold. So this time your task is to find a counter-example!
(The characters # in front of the parentheses make the feedback easier to grasp, by forcing the parentheses to be printed even when they are unnecessary.)



or

Listing a DFA that Represents an Integer Arithmetic Expression or Formula

Here you can ask MathCheck to construct a DFA from an expression or a formula. The result comes as a listing. The box contains an example formula, but you may delete it to write your own.

or