D23 Rule-based Prover: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Im06r
imported>Im06r
Line 21: Line 21:


http://wiki.event-b.org/index.php/All_Rewrite_Rules
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.
* 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==

Revision as of 17:58, 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.
  • 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

Available Documentation

Planning