Proof Contextual Information - Revision history

imported>Laurent: /* In the Origin was the Proof Attempt */

2010-12-15T14:09:17Z

In the Origin was the Proof Attempt

← Older revision		Revision as of 14:09, 15 December 2010
Line 25:		Line 25:

	There is currently already a contextual information available to tactics from a proof tree node, which is the proof attempt given as origin to the proof tree. This information is put into the proof tree in every situation where a tactic could be called on the proof tree. It can then be asserted that the origin of a proof tree received by a tactic is the corresponding proof attempt.		There is currently already a contextual information available to tactics from a proof tree node, which is the proof attempt given as origin to the proof tree. This information is put into the proof tree in every situation where a tactic could be called on the proof tree. It can then be asserted that the origin of a proof tree received by a tactic is the corresponding proof attempt.
	The following is a code ~~excerpt that can be used~~ to fetch a PO sequent from a proof tree node:
			The following is a code snippet showing how to fetch a handle to the PO sequent from a proof tree node:
	<pre>		<pre>
	public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {		public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {

imported>Laurent: /* Handling Rule Validity with Reasoners */

2010-12-15T13:43:54Z

Handling Rule Validity with Reasoners

← Older revision		Revision as of 13:43, 15 December 2010
Line 20:		Line 20:
	For reasoners to remain sound in whatever context at whatever time, it is their own duty to verify the validity of this input. Thus, if tactics pass rules through their input, and these rules are liable to become invalid (changed or removed), a reasoner must verify their validity before applying them. This could be achieved with a global registry of currently valid rules, updated during deployments.		For reasoners to remain sound in whatever context at whatever time, it is their own duty to verify the validity of this input. Thus, if tactics pass rules through their input, and these rules are liable to become invalid (changed or removed), a reasoner must verify their validity before applying them. This could be achieved with a global registry of currently valid rules, updated during deployments.

	The problem of updating proof states after a clean can be solved by these very reasoners, if they visibly bear their particularity (of not always being reusable). They could implement a special interface, say '''~~IUncertainReuseReasoner~~''' with a method '''isReusable'''(IReasonerInput input). This method would be called when checking proof reusability at proof status update time.		The problem of updating proof states after a clean can be solved by these very reasoners, if they visibly bear their particularity (of not always being reusable). They could implement a special interface, say '''IIrregularReasoner''' with a method '''isReusable'''(IReasonerInput input). This method would be called when checking proof reusability at proof status update time.

	== In the Origin was the Proof Attempt ==		== In the Origin was the Proof Attempt ==

imported>Laurent: /* Handling Context with Tactics */

2010-12-15T13:40:43Z

Handling Context with Tactics

← Older revision		Revision as of 13:40, 15 December 2010
Line 12:		Line 12:
	== Handling Context with Tactics ==		== Handling Context with Tactics ==

	Thus, contextual informations have to be handled in tactics. They ~~have~~ a proof tree node as parameter, so all ~~informations~~ should be available from this starting point. After fetching and processing these data, a tactic can ~~the~~ specify the intended behaviour of the called reasoner(s) via reasoner input(s). For instance, when a rule-based prover tactic knows which theory is being proved and which rules are applicable, these rules can be encapsulated in the reasoner input passed to the reasoner. The reasoner then only applies the given rules, regardless of any external notion.		Thus, contextual informations have to be handled in tactics. They take a proof tree node as parameter, so all information should be available from this starting point. After fetching and processing these data, a tactic can specify the intended behaviour of the called reasoner(s) via reasoner input(s). For instance, when a rule-based prover tactic knows which theory is being proved and which rules are applicable, these rules can be encapsulated in the reasoner input passed to the reasoner. The reasoner then only applies the given rules, regardless of any external notion.

	Similarly, when the user profile metatactic knows which project it is applied to, it can call the project-specific profile metatactic.		Similarly, when the user profile metatactic knows which project it is applied to, it can call the project-specific profile metatactic.

imported>Laurent at 13:38, 15 December 2010

2010-12-15T13:38:22Z

← Older revision		Revision as of 13:38, 15 December 2010
Line 1:		Line 1:
	The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, prover behaviours were only determined by a sequent and optionally a user input. Several features of the platform now require extra ~~informations~~:		The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, prover behaviours were only determined by a sequent and optionally a user input. Several features of the platform now require extra information:
	* project specific tactic profiles need the project of the PO		* project specific tactic profiles need the project of the PO
	* mathematical extension rules need the theory where the rule is defined		* mathematical extension rules need the theory where the rule is defined

imported>Nicolas: New page: The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case...

2010-12-14T15:34:36Z

New page: The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case...

New page

The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, prover behaviours were only determined by a sequent and optionally a user input. Several features of the platform now require extra informations:
* project specific tactic profiles need the project of the PO
* mathematical extension rules need the theory where the rule is defined
* rule-based prover needs to know whether the rules in a proof are still valid (reusable)

The last point concerns the rule-based prover as a separate plug-in as well as its equivalent in mathematical extensions. The requirement stated here is that, after a project clean, proof states must reflect the possibility to replay corresponding proofs. If a given rule has been used in a proof, and then this rule has been changed or removed, the proof status must be considered ''broken''.

== Reasoners are Context-Free ==

The concept of a reasoner is that of a purely mathematical processing unit. Hence it shall remain unaware of notions like ''project'', ''proof obligation'', or merely ''proof'' … The only notion a reasoner deals with is that of ''sequent'', along with an optional specific input.

== Handling Context with Tactics ==

Thus, contextual informations have to be handled in tactics. They have a proof tree node as parameter, so all informations should be available from this starting point. After fetching and processing these data, a tactic can the specify the intended behaviour of the called reasoner(s) via reasoner input(s). For instance, when a rule-based prover tactic knows which theory is being proved and which rules are applicable, these rules can be encapsulated in the reasoner input passed to the reasoner. The reasoner then only applies the given rules, regardless of any external notion.

Similarly, when the user profile metatactic knows which project it is applied to, it can call the project-specific profile metatactic.

== Handling Rule Validity with Reasoners ==

For reasoners to remain sound in whatever context at whatever time, it is their own duty to verify the validity of this input. Thus, if tactics pass rules through their input, and these rules are liable to become invalid (changed or removed), a reasoner must verify their validity before applying them. This could be achieved with a global registry of currently valid rules, updated during deployments.

The problem of updating proof states after a clean can be solved by these very reasoners, if they visibly bear their particularity (of not always being reusable). They could implement a special interface, say '''IUncertainReuseReasoner''' with a method '''isReusable'''(IReasonerInput input). This method would be called when checking proof reusability at proof status update time.

== In the Origin was the Proof Attempt ==

There is currently already a contextual information available to tactics from a proof tree node, which is the proof attempt given as origin to the proof tree. This information is put into the proof tree in every situation where a tactic could be called on the proof tree. It can then be asserted that the origin of a proof tree received by a tactic is the corresponding proof attempt.
The following is a code excerpt that can be used to fetch a PO sequent from a proof tree node:
<pre>
public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {
final Object origin = ptNode.getProofTree().getOrigin();
if (!(origin instanceof IProofAttempt)) {
return "tactic unapplicable without contextual information";
}
final IProofAttempt pa = (IProofAttempt) origin;
final String poName = pa.getName();
final IProofComponent pc = pa.getComponent();
final IPORoot poRoot = pc.getPORoot();
final IPOSequent sequent = poRoot.getSequent(poName);
// ...
}
</pre>