4f Checker

The SD editor has a plug-in, the 4f Checker,  which allows you to check if your derivation is mathematically correct. The checker formulates each step in the derivation as a mathematical theorem, and sends the theorem to an automatic theorem prover that runs in the cloud. The derivation is correct, if each step in the derivation is proved correct. The checker warns for each derivation step that it was not able to prove correct.

Derivation with an Error

The derivation below contains an error, the second derivation step is not correct. The checker shows a "!" as a warning sign for the incorrect step, and a check mark for the correct ones.

Corrected Derivation

Here we have corrected the erroneous step. The checker now marks each step as correct, so the whole derivation is correct.

Chips by lamdogjunkie, www.flickr.com. CC BY 2.0

How to Use the Checker

The checker will return a mark for each step in the derivation, in the right hand side column. The checker may run into different situations when checking the step:

a) The checker may report that it does not understand the derivation step. There could be a syntax error in the step,  or  you may be using mathematical notation that the checker does not know. You then need to rewrite the step.

b) The checker may report that the step is correct. Then you are fine.

c) The checker may report that it was not able to prove the step. There could be different reasons for this:

  1. The checker is not able to prove the step because it is incorrect. You need to fix the error.
  2. The checker runs out of time trying to find a proof of it. If you still believe that the step is correct, you could try to help the checker by splitting the step up into smaller steps.
  3. The checker does not know enough about the underlying mathematics to prove the step. Try to add assumptions, facts, or definitions that could make it easier for the checker to prove the step.

The checker is intended only as a help in checking your derivation. In the end, you are yourself responsible for checking that the derivation is correct. The checker gives you hints for how to find errors and create a correct solution.

Chips by lamdogjunkie, www.flickr.com. Licence CC BY 2.0

What the Checker Can Prove

The 4f Checker uses a number of different automatic theorem proving systems in parallel, to try to prove that a step is correct. These systems all have their special expertise, being good at proving theorems in some areas of mathematics, but may be quite poor for other areas. Hence, the efficiency of the checker depends on the area of mathematics that it is checking, and on the automatic theorem proving systems that are available for this area.

Areas of expertise

The checker is reasonably good in proving derivation steps in the following areas of mathematics:

  1. Polynomials  (equations, inequalities, functions)
  2. Rational expressions (arithmetic and polynomial rational expressions)
  3. Expressions with radicals (powers, square roots, fractional powers)
  4. Logarithms
  5. Exponents
  6. First order logic
  7. Basic trigonometry

Some of these areas may require more powerful theorem provers, available at an extra cost.

Using 4f Checker

The 4f Checker is available in 4f Studio and 4f Note. The checker can be used in any place where the eMath editor is used: in 4f textbooks when solving assignments, in 4f notebooks and in 4f course Books. The 4f Checker requires that the 4f Studio server is available.

You check a derivation by choosing  "check" in the checker menu. This will start the process of checking. The checker checks all derivation steps in parallel, using three or four different automatic theorem provers in parallell for each step. The checker will mark each step with either a check mark (the step is correct) or an exclamation mark (when it did not find a proof). The checker may also indicate a syntax error for a step that is does not understand. The checker menu "remove marks" will delete all checker marks.