06:5506:55, 22 February 2025diffhist+492 N
Implication inside an Existential QuantifierCreated page with " With version 1.15 ProB produces a warning if you use an implication inside an existential quantifier. Here we explain why. Take a look at <pre> f: 1..3 --> NAT & f = [0,0,0] & #i.(i:dom(f) => f(i)>0) </pre> You may be surprised to learn that the existential quantifier on the third line is true, even though no element of the array f is greater than 0. Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the imp..."
07:1707:17, 8 February 2025diffhist+694 N
ProB REPLCreated page with "== The REPL of ProB == ProB provides various consoles, also called REPL (Read-Eval-Print-Loop). A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. ProB provides various REPLs, depending on which version of ProB you use: * The REPL in probcli can be started with the command <tt>-repl</tt> * The REPL in ProB Tcl/Tk is the Eval Console. * ProB2-UI also provides a console view Below we describe th..."