Help on typing:
propositional
symbol  type comment
/\
\/
¬!
FFF
TTT
UUU(not yet implemented)
-->
<->
&&&&short-circuit and
||||short-circuit or
->>Łukasiewicz implication (not yet implemented)
**is defined (not yet implemented)
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
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)

# MathCheck Real Logic Mode

## Introduction

On this web page you can try the MathCheck real logic mode. It features full ordinary predicate logic machinery on linear real number arithmetic. “Linear” means that variables may be multiplied and divided by constants, but not by variables. Variables also cannot be used in divisors. Such operations as power, square root and trigonometric functions are not available. On the other hand, the absolute value operator is available. There are ideas of how to relax the restriction a bit in a pedagogically valuable way, but let us now focus on what is available this very moment.

Although the restriction on the arithmetic is severe, the mode can be used in problems of many types: linear equations, linear inequations, systems of linear (in)equations on many variables, and quantifier problems. A special advantage is that in many cases, the teacher may give students a problem without giving MathCheck anything. Most importantly, this applies to systems of (in)equations. Alternatively, by giving the system or its roots to MathCheck, the teacher may give students a verbally stated problem where the students first have to formalize it as a system of (in)equations and then solve it.

The underlying decision algorithm is complicated. Programming it was very challenging, and there are many places for bugs to hide. Please report bugs to AV. At the time of writing, in particular, the behaviour of the program on illegal input has been very little tested. Furthermore, the underlying decision problem is very complex. If quantifiers are used, it is much worse than NP-complete. Therefore, please be not greatly disappointed if the tool gives up because of too much work. Future dreams include adding some heuristics to improve the performance of the decision algorithm.

A term may consist of:

• natural numbers represented as nonempty strings of digits
• mixed numbers written like 2 3/4
• variables (small letters, capital letters, greek letters represented by the first two letters of their name)
• arithmetic operators +, -, *, /, (…), #(…#) (hard parentheses), |…| (absolute value).

A formula may consist of:

• chains of relations of the form t1 = t2 = … = tn, where any of <, <=, =, !=, >= and > may be used between terms
• the following constants and propositional operators: FF, TT, /\, \/, ! (not), --> and <->,
• quantifiers: AA v: φ, AA v; φ: ψ, EE v: φ, and EE v; φ: ψ, where v is any variable and φ and ψ are any formulas.

A reasoning chain may consist of:

• an optional global assumption of the form assume φ;
• one or more formulas separated by any of the reasoning operators ==>, <==, <=> and ===.

The difference between <=> and === is that <=> does and === does not treat the undefined truth value as equivalent to false. Because undefined truth values cannot (currently) arise in the real logic mode, this distinction is not important here. However, it is significant in some other modes of MathCheck. Furthermore, the dreams of how the real logic mode will be expanded in the future contain features that will make the distinction important.

If only one formula (and thus no reasoning operators) is given, MathCheck either declares it true, provides a counterexample, gives up for some reason, or does something which it should not because of a bug. Otherwise, MathCheck checks each reasoning step and either declares the chain as valid, gives a counterexample on the first invalid step, gives up for some reason, or does something which it should not because of a bug.

Please write a formula or a reasoning chain into the box above, or try any of the examples below, or (most preferably!) both. One of the submit buttons delivers feedback on a new browser tab or window, the other to the box on the right. You may change the input in the example and try again, and you may get the original input back by re-loading this web page (it may be necessary to keep the SHIFT key pressed).

## Absolute Value Examples

For your convenience, the examples are given as solved. Please also try what happens if you break the solutions and then click a submit button. Unless otherwise stated, no hidden information has been given to the tool. In those cases, the starting point of the problem can be copied to the empty answer box above and you can try there to solve the problem yourself.

Our first example illustrates that propositional operators can express analysis by case.

or

Perhaps solving the two cases simultaneously felt a bit confusing. There are more than one ways to solve them one at a time. Let us now see one that does not minimize the amount of typing, but is very clear.

or

## Set of Equations Examples

In the case of the first problem, the teacher has provided MathCheck with hidden information. So the problem can only be solved in the given answer box. Please wipe the solution out, if you want to solve it yourself.

The relationship between the Celsius and Fahrenheit temperature scales is of the form F = aC + b. Using the facts that 100°C = 212°F and −40°C = −40°F, find a and b by formulating a system of equations and solving it.

or

This problem is from George Pólya “How to Solve It”. Instead of following the laborious dull error-prone mechanical procedure, the student is asked to try and find a short cut. The solution shown below exploits a short cut.

or

Of course, if the goal of the user is not to study but just find the result, (s)he can do the following.

or

When doing so, one must remember that the tool provides a single counterexample from potentially many. The following illustrates this.

or

## Quantifier Examples

The definition of continuity proved too complicated to process, and there is also the problem that the available arithmetic machinery does not allow expressing most interesting functions. However, the tool is able to find out that a function defined as two pieces is not continuous at the border of the pieces.

or

The above example may also be tried at other points than (7, 8/3), and with the first line in the form AA ep; ep > 0:.