D23 Rule-based Prover
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 or not).
The following key points summarise the different decisions/choices that have been made:
- Contexts describe the static properties of models, and they are used to parameterise machines. Adding the capability of defining proof rules within contexts would allow the co-existence of modelling elements and meta-logical elements with no clear relationship between the two. This may require significant changes to the core architecture, and will unnecessarily overload the functionality of contexts with elements not directly relevant to modelling. As such, a clear separation of modelling and meta-reasoning was adopted. This resulted in a theory construct that acts as a placeholder for prover extensions.
- Rodin has a collection of rewrite and inference rules. Most inference rules as found in
http://wiki.event-b.org/index.php/Inference_Rules require predicate variables to be defined. This is not the case for most rewrite rules as found in
http://wiki.event-b.org/index.php/All_Rewrite_Rules .
Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.
