Proof Manager - Revision history

imported>Ladenberger: /* Overview */

2011-10-27T10:33:23Z

Overview

← Older revision		Revision as of 10:33, 27 October 2011
Line 3:		Line 3:
	== Overview ==		== Overview ==

	Proof obligations are generated by the proof obligation generator and have the form of ''[[sequents]]''.		Proof obligations are generated by the proof obligation generator and have the form of ''[http://handbook.cobra.cs.uni-duesseldorf.de/current/html/sequents.html sequents]''.

	Sequents are proved using ''[[Proof Manager#Proof Rules\|proof rules]]''.		Sequents are proved using ''[[Proof Manager#Proof Rules\|proof rules]]''.
Line 14:		Line 14:

	In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of ''[[Proof Manager#Tactics\|tactics]]''. They provides high-level strategic proof manipulations. Adding new tactics is the second possibility for extending the Proof Manager.		In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of ''[[Proof Manager#Tactics\|tactics]]''. They provides high-level strategic proof manipulations. Adding new tactics is the second possibility for extending the Proof Manager.



	== Proof Rules ==		== Proof Rules ==

imported>Ladenberger: /* Tactics */

2011-10-27T10:31:27Z

Tactics

← Older revision		Revision as of 10:31, 27 October 2011
Line 142:		Line 142:

	== Tactics ==		== Tactics ==
	''Tactics'' provide an easier way to construct and manage proof search and manipulation. They provide calls to the underlying [[reasoners]] or other tactics to modify proofs.		''Tactics'' provide an easier way to construct and manage proof search and manipulation. They provide calls to the underlying [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html reasoners] or other tactics to modify proofs.

	The input of a tactic is a proof tree node which will be used as the point of application. The output of a tactic is a boolean to indicate if it is successful or not.		The input of a tactic is a proof tree node which will be used as the point of application. The output of a tactic is a boolean to indicate if it is successful or not.

imported>Ladenberger: /* Basic Tactics */

2011-10-27T10:31:16Z

Basic Tactics

← Older revision		Revision as of 10:31, 27 October 2011
Line 155:		Line 155:
	* '''Prune''' A direct application of the pruning facility providing by the proof tree. The tactic is successful if the input node are non-pending.		* '''Prune''' A direct application of the pruning facility providing by the proof tree. The tactic is successful if the input node are non-pending.

	* '''Rule Application''' Tactics of this class provide a wrapper around a proof rule (See [[Proof Rules]]). The tactic is successful if the proof rule is successful applied to the input node.		* '''Rule Application''' Tactics of this class provide a wrapper around a proof rule (See [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/proof_rules.html Proof Rules]). The tactic is successful if the proof rule is successful applied to the input node.

	* '''Reasoner Application''' Tactics of this class provide a wrapper around a reasoner (See [[Reasoner]]). The tactic is successful if the reasoner is successful applied to the input node.		* '''Reasoner Application''' Tactics of this class provide a wrapper around a reasoner (See [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html Reasoner]). The tactic is successful if the reasoner is successful applied to the input node.

	=== Tactical Tactics ===		=== Tactical Tactics ===

imported>Ladenberger: /* Reasoners */

2011-10-27T10:30:48Z

Reasoners

← Older revision		Revision as of 10:30, 27 October 2011
Line 72:		Line 72:

	== Reasoners ==		== Reasoners ==
	Reasoners are responsible for generating [[Proof Rules]]. The input of a reasoner is:		Reasoners are responsible for generating [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/proof_rules.html Proof Rules]. The input of a reasoner is:

	1. A sequent.		1. A sequent.

imported>Ladenberger: /* Representation */

2011-10-27T10:28:45Z

Representation

← Older revision		Revision as of 10:28, 27 October 2011
Line 35:		Line 35:
	* '''antecedents''' A list of antecedents (to be explain later).		* '''antecedents''' A list of antecedents (to be explain later).

	* '''reasoner''' the reasoner used to generate this proof rule (See [[reasoners]]).		* '''reasoner''' the reasoner used to generate this proof rule (See [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html reasoners]).

	* '''reasoner input''' the input to the reasoner to generate this proof rule (See [[reasoners]]).		* '''reasoner input''' the input to the reasoner to generate this proof rule (See [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html reasoners]).

	Each antecedent of the proof rule contains the following information:		Each antecedent of the proof rule contains the following information:

imported>Mathieu: Category:Proof

2009-08-12T12:52:27Z

Category:Proof

← Older revision		Revision as of 12:52, 12 August 2009
Line 172:		Line 172:
	[[Category:Design]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]
			[[Category:Proof]]

imported>Son: /* Proof Rules */

2008-12-28T11:21:01Z

Proof Rules

← Older revision		Revision as of 11:21, 28 December 2008
Line 47:		Line 47:
	With this representation, a proof rule in Rodin corresponding to a proof schema as follows:		With this representation, a proof rule in Rodin corresponding to a proof schema as follows:

	{{InfRule\|\|<math>\frac{\quad H, H_u, H_{A_0} \vdash G_{A_0} ~~~\ldots~~~ H, H_u, H_{~~A_0~~} \vdash G_{~~A_0~~}\quad}{H, H_u \vdash G_u}</math>}}		{{InfRule\|\|<math>\frac{\quad H, H_u, H_{A_0} \vdash G_{A_0} ~~~\ldots~~~ H, H_u, H_{A_n} \vdash G_{A_n}\quad}{H, H_u \vdash G_u}</math>}}

	Where:		Where:
Line 64:		Line 64:
	Given a proof rule of the form mentioned above, the following describes how to apply this rule to an input ''sequent''. The result of this process is a list of output sequents if successful or ''null'' otherwise.		Given a proof rule of the form mentioned above, the following describes how to apply this rule to an input ''sequent''. The result of this process is a list of output sequents if successful or ''null'' otherwise.

	* The rule is applicable if the goal of the sequent is not exactly the same as the ''used goal'' or any of the ''used hypotheses'' is not contained in the set of hypotheses of the input sequent.		* The rule is NOT applicable if the goal of the sequent is not exactly the same as the ''used goal'' or any of the ''used hypotheses'' is not contained in the set of hypotheses of the input sequent.

	* In the case of applicable, the antecedent sequents are returned. The goal of each antecedent sequent is the ''new goal'' correspondingly. The hypotheses of each antecedent sequent is the union of the old hypotheses and ''added hypotheses'' of the corresponding antecedent.		* In the case of applicable, the antecedent sequents are returned. The goal of each antecedent sequent is the ''new goal'' correspondingly. The hypotheses of each antecedent sequent is the union of the old hypotheses and ''added hypotheses'' of the corresponding antecedent.

imported>Mathieu: Cat:design

2008-10-30T14:20:49Z

Cat:design

← Older revision		Revision as of 14:20, 30 October 2008
Line 170:		Line 170:
	More complex proof strategy can be constructed by recursively applying the above tactical tactics.		More complex proof strategy can be constructed by recursively applying the above tactical tactics.

	[[Category:~~Developer documentation~~]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Mathieu: /* Sequents */ redondant with sequents

2008-10-02T21:08:24Z

Sequents: redondant with sequents

← Older revision		Revision as of 21:08, 2 October 2008
Line 15:		Line 15:
	In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of ''[[Proof Manager#Tactics\|tactics]]''. They provides high-level strategic proof manipulations. Adding new tactics is the second possibility for extending the Proof Manager.		In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of ''[[Proof Manager#Tactics\|tactics]]''. They provides high-level strategic proof manipulations. Adding new tactics is the second possibility for extending the Proof Manager.

	~~== Sequents ==~~
	~~A sequent stands for something we want to prove.~~

	~~Sequents are of the following form~~

	~~<math>H \vdash G</math>~~

	~~where '''H''' is the set of hypotheses (predicates) and '''G''' is the goal (a predicate in the mathematical language).~~

	~~The meaning of the above sequent is that: ''Under the hypotheses H, prove the goal G''.~~

	== Proof Rules ==		== Proof Rules ==

imported>Mathieu: /* Overview */ link to sequents

2008-10-02T21:07:58Z

Overview: link to sequents

← Older revision		Revision as of 21:07, 2 October 2008
Line 3:		Line 3:
	== Overview ==		== Overview ==

	Proof obligations are generated by the proof obligation generator and have the form of ''[[~~Proof Manager#Sequents\|~~sequents]]''.		Proof obligations are generated by the proof obligation generator and have the form of ''[[sequents]]''.

	Sequents are proved using ''[[Proof Manager#Proof Rules\|proof rules]]''.		Sequents are proved using ''[[Proof Manager#Proof Rules\|proof rules]]''.