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
• ADVANCE D3.3 Improvement of automated proof
  ...e the diversity of predicates and increase the automated proofs of trivial proof obligations often encountered in degenerated cases (that is not interesting The proportion of automatically discharged proof obligations heavily depends on the auto-tactic configuration. Sometimes, th
  7 KB (1,145 words) - 10:05, 8 October 2013
• 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 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
• Extending the Proof Obligation Generator(How to extend Rodin Tutorial)
  ...[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|Generating the proof obligations]]}} ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand
  13 KB (1,774 words) - 13:57, 5 September 2013
• Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
  ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand ...oof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
  13 KB (1,755 words) - 07:19, 7 September 2010

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
• 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
• Scenarios for Merging Proofs
  == Proof structure == With respect to the merging objective, a proof is made of:
  6 KB (1,046 words) - 10:34, 27 October 2011
• Generic Instantiation
  ...xtending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development r ...n the instantiation. In that sense our approach avoids re-proof of pattern proof obligations in the instantiation. The reusability of a development is expre
  2 KB (232 words) - 15:23, 4 July 2013
• 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 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 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
• Refactoring Framework Release History
  ...). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem ** Renaming of proofs would not save the proof files after renaming
  2 KB (357 words) - 12:18, 8 June 2010
• SMT Plug-in Performance
  Performance is measured by running the SMT solvers on a set of proof obligations coming from some Event-B projects. Each solver is run in the ex :contains proof obligations to test, organized in Event-B projects
  4 KB (652 words) - 08:48, 6 June 2014
• D23 Improvements to Existing Provers
  ...html One point rule], arithmetic rules), have been added to discharge more proof obligations more easily. * Reducing proof storage space.
  5 KB (789 words) - 11:41, 27 January 2010
• Modeling Feedback
  Real goal is to obtain a proof, not a model. The model is only our mean of choice to obtain a proof.
  1 KB (153 words) - 13:44, 28 October 2008
• Disprover
  or proofs for a given proof obligation. ...ult. In this cases, the absence of a counter-example will be reported as a proof.
  1 KB (155 words) - 13:34, 2 May 2016
• Revisiting Feasibility POs
  in the Proof Obligation Generator (POG) of Rodin 2.3 where one could have an event-B project containing two machines where all proof obligations are
  8 KB (1,284 words) - 18:33, 30 January 2012
• How to read Rodin projects and elements programmatically
  ==How to read Proof Obligations== For information on reading proof obligations, have a look at [[Accessing Proof Obligations]].
  3 KB (314 words) - 14:12, 30 May 2009
• Dagstuhl Seminar 2009
  * Proof automation * Proof reuse
  1 KB (150 words) - 13:31, 3 November 2009
• ADVANCE D3.2 Language extension
  ...with these additional notations, the user can also define new proof rules (proof extensions). ..., validating and using extensions while exploiting the benefits brought by proof obligations.
  4 KB (642 words) - 08:33, 29 June 2012
• Versioned Reasoners
  ...This entails potential problems: what happens if we try to reuse/replay a proof rule serialized by the old reasoner implementation ? There might be unexpec ...en trying to reuse them. Rather than adding yet another xml attribute into proof files, it has been decided to concatenate the version to the reasoner name,
  2 KB (308 words) - 17:01, 20 November 2009
• Flows
  ...as writing and maintaining deadlock-freedom and relative deadlock freedom proof obligations. Its core functionality is concerned with the verification of t ...rs and thus there will be always some delays between saving a diagram and proof status update.
  4 KB (630 words) - 22:31, 22 January 2011
• Language of an Event-B Component
  As concerns generated files (e.g., statically checked files and proof obligation files), they contain formulas in the same language as the compon Proof status files do not contain any formula and are therefore independent on th
  4 KB (692 words) - 15:06, 20 November 2013
• SMT 1.4 Performance Results
  This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually. ...provers have individually improved their rate of automatically discharged proof obligations.
  2 KB (281 words) - 15:57, 11 September 2017
• ADVANCE D3.3 Language extension
  ...with these additional notations, the user can also define new proof rules (proof extensions). ..., validating and using extensions while exploiting the benefits brought by proof obligations.
  4 KB (648 words) - 14:52, 7 October 2013
• Flows Plug-in
  ...the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of t ...isprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.
  4 KB (699 words) - 17:36, 3 December 2010
• D23 Flow Plug-in
  ...of the Flows plug-in. The primary reason to offer such a weak guarantee is proof effort required for stronger types of connectives. ...and the proof obligations related to flow appear in the list of the model proof obligations.
  4 KB (609 words) - 11:37, 8 January 2010
• 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
• Developer Documentation
  * [[Accessing Proof Obligations]] * [[Extending the Proof Manager]]
  2 KB (179 words) - 09:17, 20 November 2013
• Single View Design
  ...''Obligation Explorer'' displays the proof obligations together with their proof state. ...original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of th
  5 KB (842 words) - 18:35, 26 March 2010
• Event-B
  ...resent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
  306 bytes (47 words) - 09:57, 4 March 2009
• Development of a flash-based filestore
  ...s an open and extensible toolset for Event-B specification, refinement and proof. The flash file system is a complex system that is challenging to specify a === Modelling and proof of a Tree-structured File System===
  4 KB (656 words) - 13:06, 18 November 2010
• Rodin
  ...[Event-B]] that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is f
  491 bytes (67 words) - 14:18, 19 September 2011
• Past Developments
  ...owing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position. ====Fixing Proof Obligations====
  6 KB (915 words) - 16:57, 27 February 2014
• Rodin Platform
  [[Rodin Proof Tactics]]
  310 bytes (38 words) - 10:51, 27 October 2011
• Plug-in Tutorial
  ...ow_to_extend_Rodin_Tutorial)|8 Generating proof obligations (Extending the Proof Obligation Generator)}}
  4 KB (487 words) - 14:27, 5 September 2013
• Rodin Plug-ins
  === Theory and Proof === * [[Isabelle for Rodin]]: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
  5 KB (757 words) - 16:19, 13 February 2020
• Event-B Qualitative Probability User Guide
  ** New proof obligations: '''PRV''', '''BND''', '''FINACT'''. === Proof Obligations ===
  6 KB (749 words) - 17:54, 21 March 2018
• Isabelle for Rodin
  This plug-in provides an automated proof tactic based on the theorem prover [http://isabelle.in.tum.de/index.html Is It also allows users to export proof obligations to Isabelle theories for later inspection with Isabelle.
  9 KB (1,317 words) - 10:07, 29 April 2013
• Rodin Platform 1.3.1 Release Notes
  Bug 2999977: Can not save proof after functional image simplification
  651 bytes (84 words) - 18:41, 22 February 2011
• Context Diagram
  ...(given properties about the constants) and Theorems (assertions requiring proof) may be attached to the ClassTypes. ClassTypes either define ‘carrier’
  606 bytes (84 words) - 20:27, 10 September 2008
• Group refinement
  ...ive laws result in a more natural and compact model with fewer and simpler proof obligations. ...sequential composition through refinement steps may result in unmanageable proof obligations. It is also more difficult to conduct subsequent refinement of
  5 KB (777 words) - 23:20, 6 December 2010
• ADVANCE D3.3 Introduction
  ...within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the second period of the ADVANCE project (Sept 2012 - Sept 2013), ...work package tasks: general platform maintenance, improvement of automated proof, model checking, language extension, model composition and decomposition.
  2 KB (325 words) - 17:32, 29 November 2013
• D23 Rule-based Prover
  ...ule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs. *Theory construct, where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied
  5 KB (796 words) - 11:44, 8 January 2010
• ADVANCE D3.3 Revised Roadmap
  ...et shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of th ...out in WP4. However, they may require some evolution of the modelling and proof tools to be performed within WP3.
  4 KB (677 words) - 16:41, 2 December 2013
• Predicate Variables Extension
  The aim of this extension is to allow defining proof rules for the Rule Based Prover using meta-variables as predicate placehold For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.
  3 KB (431 words) - 15:14, 18 February 2010
• Rodin Platform Welcome Page
  ...formal method and provides natural support for refinement and mathematical proof. To improve your proof experience, please install the third-party provers from Atelier B. This is
  2 KB (322 words) - 16:45, 20 April 2010
• Rodin Developer Support
  * [[Proof Purger Design|Proof Purger]] allows to delete unused proofs. * [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
  8 KB (1,260 words) - 12:45, 30 July 2015
• Theory Plug-in
  ...ent to define rewrite rules to a versatile platform to define and validate proof and language extensions. ...n be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
  7 KB (958 words) - 14:53, 14 June 2021
• D32 Mathematical Extensions
  ...types. Along with these additional notations, the user can also define new proof rules (prover extensions). ...es and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. W
  7 KB (1,095 words) - 14:40, 21 December 2010
• ADVANCE D3.2 Introduction
  ...within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011) ...ed into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decompositio
  2 KB (371 words) - 16:27, 13 July 2012
• Maplet Overriding in Goal
  ...imes the expression ''x''. If this expression is big, then it can make the proof rule hard to read. ...te of the conjunction is provable. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writ
  5 KB (824 words) - 16:05, 18 March 2014
• D32 General Platform Maintenance
  * Proof replay on undischarged POs (since release 1.3) ...e slightly changed and need to be discharged again. However, replaying the proof for these POs could most of the time be enough to discharge it. Hence, a co
  9 KB (1,423 words) - 16:28, 14 November 2011
• Generic Instantiation Plug-in User Guide
  ...from the instantiated machines where it is avoided the re-proof of pattern proof obligations. Afterwards <math>GI_n</math> can be further refined to <math>P
  5 KB (720 words) - 15:20, 4 July 2013
• Datatype Rules
  The resulting proof step is The resulting proof step is
  8 KB (1,199 words) - 13:37, 7 September 2010
• Rodin File Types
  |<tt>.bpo</tt> || {{class|IPORoot}} || Event-B Proof Obligations || Event-B Core |<tt>.bps</tt> || {{class|IPSRoot}} || Event-B Proof Statuses || Event-B Core
  3 KB (449 words) - 14:55, 12 March 2019
• Rodin Workshop 2012
  ...et for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A ran * How to create and use custom/parameterized proof tactics (Systerel/Jean-Raymond Abrial), 30 mins
  4 KB (530 words) - 15:34, 23 March 2012
• Scenarios for Team-based Development
  ...instance that if we change an invariant, that not the whole prooftree of a proof is invalidated, but only a subtree. ...sions.) There are, however, still issues with how to manage the individual proof files in case of changes to the model (renaming of some files, deletion of
  4 KB (670 words) - 14:38, 29 January 2009
• D32 Teamwork
  ...ected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also refe ...be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable deco
  5 KB (780 words) - 11:22, 21 December 2010
• How To Evolve Reasoners
  ...volve in time, to fix bugs or modify the behaviour, or to match additional proof rules, even after the old implementation was used to prove models. This lea ...ion will be left unnoticed. Thus, if we clean a project in order to update proof statuses, these proofs will be considered reusable (in the sense of org.eve
  4 KB (642 words) - 10:29, 27 October 2011
• ADVANCE Deliverable D3.3
  ...the ADVANCE Deliverable D3.3 (Methods and tools for model construction and proof II) which will be delivered to the European Commission at month 24 (2013-09 #to provide expert formal proof support to the industrial partners;
  6 KB (830 words) - 13:21, 7 October 2013
• Group refinement plugin
  ...tract variables and events retained solely for the needs of the refinement proof and those preserved as an integral part of an overall specification in the ...by auxiliary variables) but rather taken into the account when generating proof obligations.
  7 KB (1,109 words) - 15:33, 31 August 2010
• Rodin Platform 2.2.2 Release Notes
  ...nc=detail&aid=3370087&group_id=108850&atid=651669 Bug 3370087: Cannot save proof with ae] :fixed proof loading (and replay) problems
  4 KB (515 words) - 08:41, 1 August 2011
• D23 Pattern Plug-in
  ...ncludes the achievements of the pattern and is correct without proving any proof obligation. ...he current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects i
  6 KB (1,034 words) - 14:43, 27 January 2010
• Rodin Platform 3.3 Release Notes
  ...'' reasoner no longer considers hidden hypotheses. This avoids leading the proof to a dead-end. === Better proof reuse ===
  7 KB (1,079 words) - 13:54, 12 July 2017
• Rewriting rules for event model decomposition
  ...Event-B assignments. Two actions are considered as being equivalent if the proof obligations generated for these actions are logically equivalent. ...o be proved (see the section related to the [[Event_Model_Decomposition#po|proof obligations]] in the event model decomposition).
  10 KB (1,604 words) - 09:19, 27 October 2011
• D32 Introduction
  ...sh the soundness of provers and improve the generation of well-definedness proof obligations,
  3 KB (415 words) - 17:03, 24 November 2010
• Modularisation Plug-in Release Notes
  * There is a bug in showing interface proof obligations - these are not refreshed automtically in the project explorer. * No proof obligations are generated to ensure deadlock freeness of event groups reali
  4 KB (601 words) - 23:58, 13 October 2009
• Old Flow Plug in page
  ...tronger types of connectives. Let us see what it means to provide a formal proof for the various cases of sequential event composition. ...g "immediately after" <math>m</math> times there would be <math>m*n</math> proof obligations. Even if only a small fraction of these result in interactive p
  11 KB (1,869 words) - 23:48, 21 January 2011
• Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
  ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand ...oof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
  13 KB (1,755 words) - 07:19, 7 September 2010
• Rodin Workshop 2023
  effective support for modelling and automated proof. The platform is open * Proof automation for Event-B theories — ''P. Rivière, N. K. Singh, Y. Aït-Ame
  3 KB (375 words) - 15:36, 26 May 2023
• Rodin Platform 3.1 Release Notes
  ...valid reasoner (old version or not installed) is properly displayed in the Proof Skeleton View. ...been used; running 'Proof Replay on Undischarged POs' will replay the old proof with the current version of the reasoner.
  6 KB (909 words) - 13:48, 17 December 2014
• Event-B Mathematical Language
  *A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as [ftp://ftp.inf.ethz.ch/pub/publica
  1 KB (203 words) - 11:28, 23 January 2014
• Adding Reasoners(How to extend Rodin Tutorial)
  ..._Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index) ...I that paint their applications in red on formulas) in case of interactive proof.<br>
  13 KB (2,012 words) - 15:43, 21 September 2021
• ADVANCE D3.3 Improvement of automated proof
  ...e the diversity of predicates and increase the automated proofs of trivial proof obligations often encountered in degenerated cases (that is not interesting The proportion of automatically discharged proof obligations heavily depends on the auto-tactic configuration. Sometimes, th
  7 KB (1,145 words) - 10:05, 8 October 2013
• Sequent Prover Developer Guide
  ...uent prover is a plug-in for the Eclipse platform which provides different proof rules to be used within the Rodin Tool. The following sections discuss the == Proof Rules ==
  17 KB (2,378 words) - 09:48, 17 June 2010
• Rodin Platform 3.8 Release Notes
  805 IAE when loading proof 807 Proof information view text cut off
  5 KB (775 words) - 12:00, 4 April 2023
• D32 Provers
  ...domains and observed that his tactic significantly increases the number of proof obligations proved automatically. ...nstruction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions
  11 KB (1,699 words) - 15:25, 27 January 2011
• D23 Decomposition
  ...to deal with a growing number of events, state variables, and consequently proof obligations. ...management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
  6 KB (825 words) - 13:27, 27 January 2010
• Theory Release History
  ** A proof obligation is generated for the well-definedness condition of recursive ope ** Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
  8 KB (1,015 words) - 13:50, 1 April 2022
• Refactoring Framework
  ...renaming an element doesn't modify their existing proof state (no loss of proof). Since there are proof obligations associated with Event-B files, while renaming the goal would be
  11 KB (1,773 words) - 07:41, 12 January 2016
• Rodin Proving Perspective
  When proof obligations (POs) are not discharged automatically the user can attempt to ...es, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views
  27 KB (4,348 words) - 08:56, 26 September 2011
• The Proving Perspective (Rodin User Manual)
  When proof obligations (POs) are not discharged automatically the user can attempt to ...es, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views
  27 KB (4,348 words) - 18:45, 28 September 2011
• Extending the Proof Obligation Generator(How to extend Rodin Tutorial)
  ...[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|Generating the proof obligations]]}} ...provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand
  13 KB (1,774 words) - 13:57, 5 September 2013
• Event-B Examples
  ...ns the abstract Event-B development, however the implementation refinement proof is ongoing. The slides outline the use of Rodin in the proof of Well-ordering theorem. The archive contains the
  9 KB (1,283 words) - 13:58, 5 July 2017

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