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 t₁ = t₂ = … = t_n, 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.

Set of Equations Examples

Quantifier Examples

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:.