Difference between revisions of "D23 Rule-based Prover"
imported>Im06r |
imported>Im06r |
||
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
[[Category:D23_Deliverable]] | [[Category:D23_Deliverable]] | ||
==Overview== | ==Overview== | ||
| + | |||
| + | The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs. | ||
| + | |||
| + | The rule-based prover plug-in has two important components: | ||
| + | *The Theory construct: where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied automatically, interactively or both. | ||
| + | *Prover Extension: which is responsible for checking what rules are applicable and applying them. | ||
| + | |||
| + | The plug-in supports the definition and validation of rewrite rules. It is expected that the plug-in will also support defining inference rules. | ||
| + | |||
| + | The University of Southampton was responsible for the development of the rule-based prover. | ||
==Motivations== | ==Motivations== | ||
| + | |||
| + | Extensibility is a major concern for theorem provers. The Rodin proving infrastructure offers an extensible mechanism where proof rules can be added and external provers can be plugged-in. However, it has the following limitations: | ||
| + | * In order to add a new proof rule, it is required to implement a rule schema (i.e., a reasoner) and a wrapper tactic. Therefore, a certain level of competence with the Java programming language as well as knowledge of Rodin architecture is necessary; | ||
| + | *After a new rule is added, soundness of the prover augmented with the new rule has to be established. It is not clear how this can be achieved at the level of Java code. | ||
| + | |||
| + | The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available at: | ||
| + | |||
| + | http://wiki.event-b.org/index.php/All_Rewrite_Rules | ||
| + | |||
| + | The advantages of the rule-based prover include: | ||
| + | |||
| + | * The rule-based prover unifies the way automatics and interactive rules are defined since this is literally specified by two toggle buttons. | ||
| + | * The addition and validation of new proof rules brings a degree of meta-reasoning to Rodin, and removes the need for Java code when adding rules. | ||
| + | * The theory construct provide a platform where prover extensions and (in the future) language extensions can be specified. | ||
| + | * Carefully checked library of rules can be provided. | ||
==Choices/Decisions== | ==Choices/Decisions== | ||
| + | The main decisions that had to be made regarding the rule-based prover include the following: | ||
| + | • Whether to use contexts as a vehicle for defining rules; | ||
| + | • What kind of rules should the theory cover first; | ||
| + | • How the meta-variables within rules are recognised (automatic type inference) | ||
==Available Documentation== | ==Available Documentation== | ||
==Planning == | ==Planning == | ||
Revision as of 18:23, 26 November 2009
Overview
The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs.
The rule-based prover plug-in has two important components:
- The Theory construct: where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied automatically, interactively or both.
- Prover Extension: which is responsible for checking what rules are applicable and applying them.
The plug-in supports the definition and validation of rewrite rules. It is expected that the plug-in will also support defining inference rules.
The University of Southampton was responsible for the development of the rule-based prover.
Motivations
Extensibility is a major concern for theorem provers. The Rodin proving infrastructure offers an extensible mechanism where proof rules can be added and external provers can be plugged-in. However, it has the following limitations:
- In order to add a new proof rule, it is required to implement a rule schema (i.e., a reasoner) and a wrapper tactic. Therefore, a certain level of competence with the Java programming language as well as knowledge of Rodin architecture is necessary;
- After a new rule is added, soundness of the prover augmented with the new rule has to be established. It is not clear how this can be achieved at the level of Java code.
The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available at:
http://wiki.event-b.org/index.php/All_Rewrite_Rules
The advantages of the rule-based prover include:
- The rule-based prover unifies the way automatics and interactive rules are defined since this is literally specified by two toggle buttons.
- The addition and validation of new proof rules brings a degree of meta-reasoning to Rodin, and removes the need for Java code when adding rules.
- The theory construct provide a platform where prover extensions and (in the future) language extensions can be specified.
- Carefully checked library of rules can be provided.
Choices/Decisions
The main decisions that had to be made regarding the rule-based prover include the following: • Whether to use contexts as a vehicle for defining rules; • What kind of rules should the theory cover first; • How the meta-variables within rules are recognised (automatic type inference)
