For this example we try and use the REPL (Read-Eval-Print-Loop) of ProB to prove theorems. The REPL can either be started using probcli's command -repl or by starting the Eval Console in ProB Tcl/Tk.
See the beginning of Sudoku Solved in the ProB REPL for more details about how to start the REPL.
The general principle for proving a sequent Hyp |- Goal is to state the hypotheses Hyp and negate the goal. If ProB finds a solution, a counter example to the sequent exists and it cannot be proven. If ProB finds no solution, then under certain circumstances the sequent is proven, as no counter example exists.
Let us prove that from x:1..100 it follows that the equation x*x+2*x+2 = 1 has no solution:
>>> x:1..100 & not(x*x+2*x+2/=1) Existentially Quantified Predicate over x is FALSE
In this case, ProB has not generated an "enumeration warning", i.e., all cases where considered: we have a proof. In general when all variables are restricted to a finite set of values in the hypotheses, ProB can be used as a prover.
Let us now lift the finiteness restriction on x and prove the theorem for all integer values:
>>> x:INTEGER & not(x*x+2*x+2/=1)
### Warning: enumerating x : INTEGER : inf: -1 ---> -1: -1
Existentially Quantified Predicate over x is TRUE
Solution:
x = -1
Here ProB has found a counter example and the sequent is not valid. As you can see, an enumeration warning occurred; meaning that not all of the infinitely many values for x will be tried. But this warning is not relevant here as a solution was found.
Let us try and restrict x to positive values; the number of values are infinite (NATURAL is the set of mathematical natural numbers, not restricted by MAXINT):
>>> x:NATURAL & not(x*x+2*x+2/=1) Existentially Quantified Predicate over x is FALSE
Here ProB has found no solution and generated no enumeration warning: the sequent is proven.