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 limitation 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