Search results

Create the page "Proof" on this wiki! See also the search results found.

Page title matches

• Induction proof
  The proof key is the following theorem: The proof of the previous theorem is given by instantiating the key theorem with : <m
  711 bytes (121 words) - 14:11, 30 October 2008
• Proof Hints
  1. '''Description''': A brief description of the proof hints with the situation where this can be helpful. ...to select these hypotheses automatically when generating the corresponding proof obligation.
  4 KB (545 words) - 22:17, 5 March 2010
• Proof Manager
  ...le for constructing proofs and maintaining existing proofs associated with proof obligations. Proof obligations are generated by the proof obligation generator and have the form of ''[http://handbook.cobra.cs.uni-d
  9 KB (1,478 words) - 10:33, 27 October 2011
• Proof Purger
  #REDIRECT [[Proof Purger Design]]
  33 bytes (4 words) - 15:59, 6 January 2009
• Proof Simplification
  ...development aims at getting rid of this kind of needless data contained in proof files. ...t the structure of proof trees, one can have a look at the [[Proof_Manager|Proof Manager]] page.
  3 KB (496 words) - 12:58, 12 August 2009
• Proof Skeleton
  #REDIRECT [[Proof Skeleton Design]]
  35 bytes (4 words) - 16:56, 6 January 2009
• Proof Trees
  ''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components: 2. '''rule''' A proof rule (possibly ''null'')
  2 KB (365 words) - 12:52, 12 August 2009
• Accessing Proof Obligations
  *IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps. *IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.
  3 KB (443 words) - 12:53, 12 August 2009
• Extension Proof Rules
  2 KB (307 words) - 15:38, 29 November 2019
• New Proof Rules
  [[Category:Proof]]
  4 KB (738 words) - 12:53, 12 August 2009
• Proof Contextual Information
  ...) 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, * rule-based prover needs to know whether the rules in a proof are still valid (reusable)
  4 KB (600 words) - 14:09, 15 December 2010
• Proof Obligation Commands
  In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: ...rer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an ele
  3 KB (457 words) - 10:43, 18 March 2010
• Proof Purger Design
  ...sed proofs by selecting projects and/or files to purge. In addition, empty proof files are also proposed for purging. Integration of the proof purger as a popup menu is achieved in the manifest through the ''org.eclips
  3 KB (505 words) - 12:54, 12 August 2009
• Proof Purger Interface
  Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However,
  2 KB (400 words) - 10:20, 27 October 2011
• Proof Skeleton Design
  This document aims at helping developers getting into the code of the proof skeleton viewer. ...eleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a conve
  2 KB (254 words) - 12:54, 12 August 2009
• Proof Skeleton View
  ...can be used on any proof, independently of the presence of a corresponding proof obligation. Furthermore, this view allows user to see together proof rules and corresponding sequents.
  2 KB (299 words) - 12:50, 27 September 2011
• Rodin Proof Tactics
  This page contains descriptions of the available proof tactics within the RODIN Platform. ...ails explanation of the tactic, when it is applicable, give the associated proof rule. See [[Inference Rules|Inference rules]] list and [[All Rewrite Rules
  57 KB (6,150 words) - 17:25, 21 February 2012
• Extending the Proof Manager
  ...le for constructing proofs and maintaining existing proofs associated with proof obligations. There are two ways for extending the Proof Manager:
  3 KB (400 words) - 10:27, 27 October 2011
• Proof Dependencies and Reasoner Conflicts
  ..., proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for ...e proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.
  1 KB (175 words) - 14:49, 6 June 2011
• ADVANCE D3.2 Improvement of automated proof
  ...h could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactic ...time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
  4 KB (596 words) - 13:21, 18 July 2012

Page text matches

• Proof Skeleton View
  ...can be used on any proof, independently of the presence of a corresponding proof obligation. Furthermore, this view allows user to see together proof rules and corresponding sequents.
  2 KB (299 words) - 12:50, 27 September 2011
• Proof Trees
  ''Proof trees'' are recursive structure based on ''Proof Tree Nodes''. Each node has three components: 2. '''rule''' A proof rule (possibly ''null'')
  2 KB (365 words) - 12:52, 12 August 2009
• Proof Dependencies and Reasoner Conflicts
  ..., proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for ...e proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.
  1 KB (175 words) - 14:49, 6 June 2011
• Proof Skeleton Design
  This document aims at helping developers getting into the code of the proof skeleton viewer. ...eleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a conve
  2 KB (254 words) - 12:54, 12 August 2009
• All Rewrite Rules
  ==[[Extension Proof Rules]]== {{:Extension Proof Rules}}
  739 bytes (98 words) - 13:29, 26 April 2013
• Prover Diagrams
  ...ation to begin to understand the structural relationships within the RODIN proof tool. The diagrams were produced as an aid to visualising these relationshi Image:ProofStatus.png|Proof Status Diagram
  726 bytes (102 words) - 12:02, 12 August 2009
• Proof Purger Interface
  Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However,
  2 KB (400 words) - 10:20, 27 October 2011
• How Rodin Deviates from Abrial's Book
  On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</m === Proof Calculus ===
  1 KB (188 words) - 11:10, 25 January 2012
• Extension Rewrite Rules
  #REDIRECT [[Extension Proof Rules]]
  35 bytes (4 words) - 10:23, 9 September 2010
• Proof Purger
  #REDIRECT [[Proof Purger Design]]
  33 bytes (4 words) - 15:59, 6 January 2009
• Proof Skeleton
  #REDIRECT [[Proof Skeleton Design]]
  35 bytes (4 words) - 16:56, 6 January 2009
• Purging Unused Proofs
  #REDIRECT [[Proof Purger Interface]]
  36 bytes (4 words) - 16:04, 6 January 2009
• Teamwork Requirements
  == Merging of proof files == ...eat if two people work independtly on different proofs that the discharged proof obligations could be merged. A first version of
  1,010 bytes (157 words) - 10:00, 22 October 2009
• Current Proof Tree Node in UI
  ...e Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 these view do not always display t ...w does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
  4 KB (683 words) - 18:33, 16 December 2011
• Proof Simplification
  ...development aims at getting rid of this kind of needless data contained in proof files. ...t the structure of proof trees, one can have a look at the [[Proof_Manager|Proof Manager]] page.
  3 KB (496 words) - 12:58, 12 August 2009
• Accessing Proof Obligations
  *IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps. *IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.
  3 KB (443 words) - 12:53, 12 August 2009
• Induction proof
  The proof key is the following theorem: The proof of the previous theorem is given by instantiating the key theorem with : <m
  711 bytes (121 words) - 14:11, 30 October 2008
• Proof Obligation Names (Rodin User Manual)
  Next is a table describing the names of context proof obligations: Next is a table showing the name of machine proof obligations:
  4 KB (575 words) - 15:09, 15 September 2011
• Proof Hints
  1. '''Description''': A brief description of the proof hints with the situation where this can be helpful. ...to select these hypotheses automatically when generating the corresponding proof obligation.
  4 KB (545 words) - 22:17, 5 March 2010
• Proof Contextual Information
  ...) 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, * rule-based prover needs to know whether the rules in a proof are still valid (reusable)
  4 KB (600 words) - 14:09, 15 December 2010

View (previous 20 | next 20) (20 | 50 | 100 | 250 | 500)