Sequent Prover - Revision history

Jan Gruteser at 13:50, 15 May 2026

2026-05-15T13:50:35Z

← Older revision		Revision as of 13:50, 15 May 2026
Line 50:		Line 50:

	The question mark shown on transitions for external provers also indicates that they may not be executable. It is the case if too many or unsuitable hypotheses are selected for proving the goal.		The question mark shown on transitions for external provers also indicates that they may not be executable. It is the case if too many or unsuitable hypotheses are selected for proving the goal.

			==== Examples ====
			A few export examples can be found here: https://stups.hhu-hosting.de/models/sequent_prover.

Engels at 08:17, 6 January 2026

2026-01-06T08:17:34Z

← Older revision		Revision as of 08:17, 6 January 2026
Line 20:		Line 20:
	Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).		Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

	[[File:Sequent prover transitions.png\|~~700px~~]]		[[File:Sequent prover transitions.png\|800px]]

	<tt>skip_to_cont</tt> is a transition that allows you to skip the current sequent and prove it later. If it is selected here, arr ∈ &integers; ⇸ &integers; will be the next goal. <tt>CONTINUATION</tt> denotes the number of additional sequents in the proof, so now there are four sequents in total, including the current sequent.		<tt>skip_to_cont</tt> is a transition that allows you to skip the current sequent and prove it later. If it is selected here, arr ∈ &integers; ⇸ &integers; will be the next goal. <tt>CONTINUATION</tt> denotes the number of additional sequents in the proof, so now there are four sequents in total, including the current sequent.

Engels at 10:58, 5 January 2026

2026-01-05T10:58:26Z

← Older revision		Revision as of 10:58, 5 January 2026
Line 3:		Line 3:
	To discharge a proof obligation one has to prove one or more sequents, consisting of hypotheses and a goal that must be derived from the hypotheses.		To discharge a proof obligation one has to prove one or more sequents, consisting of hypotheses and a goal that must be derived from the hypotheses.

	Currently, <tt>.pl</tt> files with proof obligations can be loaded which are exported from Rodin. To generate these files, an Event-B ~~machine~~ must be selected in Rodin and the option <tt>ProB Standalone > Export POs for ProB</tt> must be invoked.		Currently, <tt>.pl</tt> files with proof obligations can be loaded which are exported from Rodin. To generate these files, an Event-B component must be selected in Rodin and the option <tt>ProB Standalone > Export POs for ProB</tt> must be invoked.

	All rules that are applicable to the current sequent are displayed in the Operations View.		All rules that are applicable to the current sequent are displayed in the Operations View.
Line 13:		Line 13:

	(Overview img)		(Overview img)

			==== Transitions ====

	Some rules require additional user input, i.e. an expression or a predicate. This is necessary, for example when it is necessary to add a new hypothesis to advance the proof, to instantiate quantifiers like the existential quantifier or perform a case distinction.		Some rules require additional user input, i.e. an expression or a predicate. This is necessary, for example when it is necessary to add a new hypothesis to advance the proof, to instantiate quantifiers like the existential quantifier or perform a case distinction.
Line 18:		Line 20:
	Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).		Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

	~~(img0)~~		[[File:Sequent prover transitions.png\|700px]]

			<tt>skip_to_cont</tt> is a transition that allows you to skip the current sequent and prove it later. If it is selected here, arr ∈ &integers; ⇸ &integers; will be the next goal. <tt>CONTINUATION</tt> denotes the number of additional sequents in the proof, so now there are four sequents in total, including the current sequent.

	==== Input Syntax ====		==== Input Syntax ====

Engels at 09:56, 1 January 2026

2026-01-01T09:56:29Z

← Older revision		Revision as of 09:56, 1 January 2026
Line 18:		Line 18:
	Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).		Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

	~~[[File:Sequent_prover_transitions.jpg]]~~		(img0)

	==== Input Syntax ====		==== Input Syntax ====
Line 25:		Line 25:
	<tt>finite(S)</tt> is an Event-B operator and is entered as <tt>S:FIN(S)</tt>.		<tt>finite(S)</tt> is an Event-B operator and is entered as <tt>S:FIN(S)</tt>.

	To illustrate a valid input, this is an example predicate for a hypothesis to be added:		To illustrate a valid input, this is an example predicate for a hypothesis to be added (x ≠ 0 &and; s ∪ t ⊂ &naturals;):

	~~(img1)~~		[[File:Sequent prover add hyp.png\|700px]]

	==== Saving Proofs ====		==== Saving Proofs ====
Line 33:		Line 33:
	To save a proof, the proof trace can be stored as a <tt>.prob2trace</tt> file (1a), which can later be reloaded and reused (1b). This option allows proofs to be revised, for example by interactively replaying the trace and modifying some steps. Alternatively, proofs can be exported as HTML documents (2):		To save a proof, the proof trace can be stored as a <tt>.prob2trace</tt> file (1a), which can later be reloaded and reused (1b). This option allows proofs to be revised, for example by interactively replaying the trace and modifying some steps. Alternatively, proofs can be exported as HTML documents (2):

	~~(img2)~~		[[File:Sequent prover proof saving.png\|800px]]

	==== Automatic Provers ====		==== Automatic Provers ====

Engels at 09:40, 1 January 2026

2026-01-01T09:40:30Z

← Older revision		Revision as of 09:40, 1 January 2026
Line 18:		Line 18:
	Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).		Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

	~~(img0)~~		[[File:Sequent_prover_transitions.jpg]]

	==== Input Syntax ====		==== Input Syntax ====

Engels at 09:34, 1 January 2026

2026-01-01T09:34:46Z

← Older revision		Revision as of 09:34, 1 January 2026
Line 22:		Line 22:
	==== Input Syntax ====		==== Input Syntax ====

	User input has to be provided in [[Summary_of_B_Syntax\|B Syntax]]. Due to syntactic differences between B and Event-B, certain operators must be adapted accordingly. For instance, a cartesian product is written as '~~<tt>~~S ** T~~</tt>~~', exponentiation as '~~<tt>~~a^b~~</tt>~~' and set difference as '~~<tt>~~S \\ T~~</tt>~~' (note that it is written as <tt>\\</tt> in the input because of the escape character <tt>\</tt>).		User input has to be provided in [[Summary_of_B_Syntax\|B Syntax]]. Due to syntactic differences between B and Event-B, certain operators must be adapted accordingly. For instance, a cartesian product is written as '''S ** T''', exponentiation as '''a^b''' and set difference as '''S \\ T''' (note that it is written as <tt>\\</tt> in the input because of the escape character <tt>\</tt>).
	<tt>finite(S)</tt> is an Event-B operator and is entered as <tt>S:FIN(S)</tt>.		<tt>finite(S)</tt> is an Event-B operator and is entered as <tt>S:FIN(S)</tt>.

Engels at 09:33, 1 January 2026

2026-01-01T09:33:22Z

← Older revision	Revision as of 09:33, 1 January 2026
Line 1:	Line 1:
		Using ProB, sequents can be proven interactively.
		For the construction of a formal proof, rules for rewriting expressions or decomposing proof goals into simpler subgoals are applied.
		To discharge a proof obligation one has to prove one or more sequents, consisting of hypotheses and a goal that must be derived from the hypotheses.

		Currently, <tt>.pl</tt> files with proof obligations can be loaded which are exported from Rodin. To generate these files, an Event-B machine must be selected in Rodin and the option <tt>ProB Standalone > Export POs for ProB</tt> must be invoked.

		All rules that are applicable to the current sequent are displayed in the Operations View.
		The implemented rules include the inference and rewrite rules available in Rodin:
		* https://wiki.event-b.org/index.php/Inference_Rules
		* https://wiki.event-b.org/index.php/All_Rewrite_Rules

		The State View shows the current sequent, including its hypotheses and goal, as well as important state properties. Furthermore, the State Visualisation presents both the current state and the preceding state, allowing a comparison between consecutive steps. By right-clicking on a predicate within this visualisation, the user can see rules that are applicable to that selected element.

		(Overview img)

		Some rules require additional user input, i.e. an expression or a predicate. This is necessary, for example when it is necessary to add a new hypothesis to advance the proof, to instantiate quantifiers like the existential quantifier or perform a case distinction.

		Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

		(img0)

		==== Input Syntax ====

		User input has to be provided in [[Summary_of_B_Syntax\|B Syntax]]. Due to syntactic differences between B and Event-B, certain operators must be adapted accordingly. For instance, a cartesian product is written as '<tt>S ** T</tt>', exponentiation as '<tt>a^b</tt>' and set difference as '<tt>S \\ T</tt>' (note that it is written as <tt>\\</tt> in the input because of the escape character <tt>\</tt>).
		<tt>finite(S)</tt> is an Event-B operator and is entered as <tt>S:FIN(S)</tt>.

		To illustrate a valid input, this is an example predicate for a hypothesis to be added:

		(img1)

		==== Saving Proofs ====

		To save a proof, the proof trace can be stored as a <tt>.prob2trace</tt> file (1a), which can later be reloaded and reused (1b). This option allows proofs to be revised, for example by interactively replaying the trace and modifying some steps. Alternatively, proofs can be exported as HTML documents (2):

		(img2)

		==== Automatic Provers ====

		In addition to interactive proving, ProB allows the invocation of external automatic provers. This can be useful for determining whether a given sequent is provable at all. The following provers can be called:

		* [[Tutorial Disprover\|the ProB (Dis-)Prover]] which searches for counterexamples and can invalidate and prove sequents
		* ProB's well-definedness prover for discharging well-definedness proof obligations
		* Atelier B's mono-lemma (ml) prover and predicate prover (pp)

		To use the Atelier B provers, the path to the <tt>krt</tt> tool must be set via <tt>File > Preferences > ATELIERB_KRT_PATH</tt>. If the provers from Atelier B were installed in Rodin, the <tt>krt</tt> executable might be found within Rodin's configuration directory (path is possibly <tt>/Users/.../rodin/configuration/org.eclipse.osgi/.../krt</tt>).

		The question mark shown on transitions for external provers also indicates that they may not be executable. It is the case if too many or unsuitable hypotheses are selected for proving the goal.

Jan Gruteser: Created blank page

2025-12-16T18:08:07Z

Created blank page

New page