Proving Theorems in the ProB REPL - Revision history

Michael Leuschel: /* Calling Other Provers */

2025-02-08T06:57:15Z

Calling Other Provers

← Older revision		Revision as of 06:57, 8 February 2025
Line 122:		Line 122:
	</pre>		</pre>

	=== ~~Calling Other Provers~~ ===		=== Reading Proof Goals from File ===

	Note, the REPL provides various ways to apply the above commands to predicates from files or to automatically generate predicates.		Note, the REPL provides various ways to apply the above commands to predicates from files or to automatically generate predicates.
Line 129:		Line 129:
	<pre>		<pre>
	>>> :prove #file=MYFILE		>>> :prove #file=MYFILE
			</pre>

			One can also apply ProB's constraint solver to a predicate (typically an implication) stored in a file without the REPL:

			<pre>
			probcli -eval_rule_file MYFILE
	</pre>		</pre>

Michael Leuschel: /* Calling Other Provers */

2025-02-08T06:54:11Z

Calling Other Provers

← Older revision		Revision as of 06:54, 8 February 2025
Line 120:		Line 120:
	Double checking proven sequent with prob(strong) after 1 ms: contradiction_found		Double checking proven sequent with prob(strong) after 1 ms: contradiction_found
	Universally quantified predicate is PROVED with [wd-krt-prover([ml],[prob(strong)])]		Universally quantified predicate is PROVED with [wd-krt-prover([ml],[prob(strong)])]
			</pre>

			=== Calling Other Provers ===

			Note, the REPL provides various ways to apply the above commands to predicates from files or to automatically generate predicates.
			For example, the following applies the WD prover to a predicate in a file named MYFILE:

			<pre>
			>>> :prove #file=MYFILE
	</pre>		</pre>

Michael Leuschel: /* Calling ProB's WD Prover */

2025-02-07T13:54:26Z

Calling ProB's WD Prover

← Older revision		Revision as of 13:54, 7 February 2025
Line 77:		Line 77:

	==== Calling ProB's WD Prover ====		==== Calling ProB's WD Prover ====
	You can call ProB's integrated prover, optimised for proving WD (well-definedness) proof obligations using the <tt>:prove</tt> command:		You can call ProB's integrated prover, optimised for [[Well-Definedness_Checking#Generating_and_Checking_Well-Definedness_Proof_Obligations_in_ProB\|proving WD (well-definedness) proof obligations]] using the <tt>:prove</tt> command:

	<pre>		<pre>

Michael Leuschel: /* Proving in the REPL */

2025-02-07T13:49:53Z

Proving in the REPL

← Older revision		Revision as of 13:49, 7 February 2025
Line 112:		Line 112:
	</pre>		</pre>


			As of version 1.15.0 of ProB, you can also call ML and ProB's WD prover together with a double-check in one command:

			<pre>
			>>> :prove-bench x:INTEGER & x>y => x>=y
			Proven by WD & [ml]
			Double checking proven sequent with prob(strong) after 1 ms: contradiction_found
			Universally quantified predicate is PROVED with [wd-krt-prover([ml],[prob(strong)])]
			</pre>

	=== User-Defined Sets ===		=== User-Defined Sets ===

Michael Leuschel at 13:43, 7 February 2025

2025-02-07T13:43:40Z

← Older revision		Revision as of 13:43, 7 February 2025
Line 1:		Line 1:
			== Proving in the REPL ==

	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 <tt>-repl</tt> or by starting the [[Eval_Console\|Eval Console in ProB Tcl/Tk]].		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 <tt>-repl</tt> or by starting the [[Eval_Console\|Eval Console in ProB Tcl/Tk]].

Michael Leuschel at 13:42, 7 February 2025

2025-02-07T13:42:45Z

@@ Line 73: / Line 73: @@
 === Calling Other Provers ===
 You can call ProB's integrated prover, optimised for proving WD (well-definedness) proof obligations using the <tt>:prove</tt> command:
@@ Line 91: / Line 93: @@
 The expectation is that no such counter-example is found (as above); if a counter-example is found an error will be raised, as we have a bug in either the prover or the constraint solver (and please send us a bug report).
 === User-Defined Sets ===

Michael Leuschel: /* Calling Other Provers */

2025-02-07T13:35:31Z

Calling Other Provers

← Older revision		Revision as of 13:35, 7 February 2025
Line 76:		Line 76:

	<pre>		<pre>
	>>> :prove x>0 => x>= 0		>>> :prove x:INTEGER & x>y => x>=y
			PROVING: x >= y
	Universally quantified predicate is PROVED with [prob-wd-prover(no_double_check)]		Universally quantified predicate is PROVED with [prob-wd-prover(no_double_check)]
	</pre>		</pre>

			You can also use the following command to double-check a proof using ProB's constraint solver.
			If the WD prover finds a proof, then the constraint solver will be launched to try and find a counter example to the proof.

			<pre>
			>>> :prove-double-check x>0 => x>=0
			Double checking proven sequent with prob(strong) after 1 ms: contradiction_found
			Universally quantified predicate is PROVED with [prob-wd-prover([prob(strong)])]
			</pre>

			The expectation is that no such counter-example is found (as above); if a counter-example is found an error will be raised, as we have a bug in either the prover or the constraint solver (and please send us a bug report).

	=== User-Defined Sets ===		=== User-Defined Sets ===

Michael Leuschel: /* User-Defined Sets */

2025-02-07T13:31:29Z

User-Defined Sets

@@ Line 70: / Line 70: @@
 PREDICATE is FALSE
 </pre>
 === User-Defined Sets ===

Michael Leuschel at 09:16, 23 December 2016

2016-12-23T09:16:50Z

@@ Line 6: / Line 6: @@
 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 <tt>x:1..100</tt> it follows that the equation <tt>x*x+2*x+2 = 1</tt> has no solution:
@@ Line 37: / Line 38: @@
 Here ProB has found no solution and generated no enumeration warning: the sequent is proven.
 === User-Defined Sets ===

Michael Leuschel at 09:19, 22 December 2016

2016-12-22T09:19:44Z

← Older revision		Revision as of 09:19, 22 December 2016
Line 37:		Line 37:

	Here ProB has found no solution and generated no enumeration warning: the sequent is proven.		Here ProB has found no solution and generated no enumeration warning: the sequent is proven.

			=== User-Defined Sets ===

			Suppose we want to prove a property not over a specific set such as the integers but over an arbitrary set.
			If you want to use additional basic types in the ProB REPL you need to define them in a B machine, they cannot (yet) be added in the REPL.
			For example, let us create a file <tt>DefSets.mch</tt>:

			<pre>
			MACHINE DefSets
			SETS D;E = {e1,e2,e3,e4,e5} // we just define two sets to be used in the REPL, D is deferred, E is enumerated
			END
			</pre>

			Then you can load the file and start the REPL:
			rlwrap probcli DefSets.mch -repl

			Let us try and prove that <tt>A={a,b} & B={c,d}</tt> implies <tt>A /\ B = {}</tt>.
			We can state this as follows. Note that in B we need to type A and B.
			Here we first use the enumerated set E for that purpose.

			<pre>
			>>> A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} )
			Existentially Quantified Predicate over A,B,a,b,c,d is TRUE
			Solution:
			A = {e1} &
			B = {e1} &
			a = e1 &
			b = e1 &
			c = e1 &
			d = e1
			</pre>

			As you can see, the goal <tt>A /\ B = {}</tt> cannot be proven, a counter-example is provided.
			If we add hypotheses that a,b,c,d are all pair-wise distinct we can prove the assertion:

			<pre>
			>>> A <: E & B<: E & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d & not( A /\ B = {} )
			Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
			</pre>

			This has used ProB’s Prolog-CLPFD solver.
			You can use ProB's translation to Z3 (see [[Using ProB with Z3]]) by prefixing the formula with <tt>z3:</tt>

			<pre>
			>>> :z3 A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
			PREDICATE is FALSE
			</pre>

			You can also translate the query to SAT via the Kodkod library (see [[Using ProB with KODKOD]]) using:

			<pre>
			>>> :kodkod A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
			kodkod ok: A = {a,b} & B = {c,d} & not(A /\ B = {}) & a /= b ... ints: none, intatoms: none
			Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).
			Times for computing solutions: []
			Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
			</pre>

			Note that ProB’s Prolog-CLPFD solver and Kodkod cannot provide proofs when you use deferred sets whose cardinality is not specified and finite.
			For example, let us use the deferred set D instead of E to type A and B:

			<pre>
			>>> A <: D & B<: D & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
			Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
			>>> D
			Expression Value =
			{D1,D2}
			</pre>

			As you can see, ProB has set the size of the set D to two (see [[Deferrred_Sets]]).
			You can see this also by asking ProB to find four different Values:

			<pre>
			>>> A <: D & B<: D & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
			Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
			</pre>

			So, in the presence of deferred sets, ProB's default solver and the Kodkod-based solver cannot be used to prove theorems; they can only be used to find counter-examples.
			The Z3 backend however does not fix the size of D:

			<pre>
			>>> :z3 A <: D & B<: D & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
			PREDICATE is TRUE
			Solution:
			A = {D1,D2}
			B = {}
			a = D1
			b = D2
			c = D3
			d = D4
			</pre>