The B-Platform

The B-Platform is the proof engine that underpins the B-Toolkit, many parts of which are implemented in the B-Theory Language (B-TL) which the B-Platform supports.

B-TL can be viewed as a kind of logic/functional programming language, whose program statements, called ``Theories'' consist of ordered sets of inference rules. A natural-deduction-style proof engine uses backwards and forwards inference to evaluate programs. Rewriting is treated as a special form of backwards inference.

A tactic language is used to add additional control to the inference mechanism.

B-TL is also the language used to supply additional user theories to the B-Toolkit's Animator and InterProver.

Although no explicit interface to the B-Platform is visible through the B-Toolkit, experienced B-Toolkit users will need to have knowledge of the syntax of B-TL and the proof mechanisms used in the B-Platform.

The B-Platform is best viewed as a ``Proof Assistant'' in constructing formal proofs. It is not a true ``Theorem Prover'', because inference rules supplied by the user do not have to be proved in terms of some basic set of axioms. The B-Platform just mechanises the application of rules, and assists with some of the house-keeping.

The B-Platform can be purchased separately from B-Core (UK) Ltd. in their product called the B-Tool (rather than B-Toolkit). It is useful for playing with and learning about proof, as well as for implementing advanced tools such as provers; the B-Platform is also sometimes referred to as the B-Kernel.

For the purposes of B-Toolkit users, a limited knowledge the syntax of a formula in B-TL is all that is required; other aspects of the language are not relevant. What follows below is not intended to be a thorough description of the B-Platform, or a complete syntax for B-TL, but rather a summary of those aspects that are essential to a working knowledge for the B-Toolkit user.

Inference Rules

An Inference Rule in B-TL is a Formula written broadly according to the syntax of the mathematical notation of AMN. An important concept is that of a ``Joker'', which is used in AMN only in the DEFINITIONS clause.

A Joker can be any single upper or lower-case letter. A Joker is true variable which can be replaced by any Formula. It is to be distinguished from AMN variables, which appear as identifiers in B-TL, which have to be at least two characters long.

Identifiers can be modified by appending a Number. This is to allow tools to create new variables when copying formulae. In the B-Toolkit, it is used to distinguish between copies of the same state variable in different contexts (inside and outside of a loop, for instance).

Three major types of rules are distinguished, `` simple rules'', `` rewrite rules'' and `` forward rules'', which, despite being syntactically similar, are applied in very different ways. Simple rules and rewrite rules are both used in backwards inference, and so are grouped as ``backward rules''.

Simple Rules

A Simple Rule has the following syntax:-

    Simple_Rule    ::= Antecedents => Consequent  |
                       Consequent

    Antecedents    ::= Antecedents & Formula      |
                       Formula

    Consequent     ::= Formula

An example of a simple rule is:-

    a <: c &
    b <: c
   =>
    a \/ b <: c

This rule states, in effect, that a goal of the form

    a \/ b <: c

can be proved if the two goals

    a <: b &
    a <: c

can both be proved.

In this example, a, b and c are Jokers which stand for any formula. So applying this rule to the goal

    STAFF \/ CUSTOMER <: PERSON

has the effect of applying the rule

    STAFF <: PERSON &
    CUSTOMER <: PERSON
   =>
    STAFF \/ CUSTOMER <: PERSON

Simple rules are used for Backwards Inference. They are applied as follows:-

The Consequent is matched to the current goal by substituting a formula for each Joker which makes the Consequent identical to the goal. If no such match can be found, the rule cannot be applied.
If the match is successful, the same substitution of formulae for Jokers is applied to the Antecedents (if any).
The current goal is replaced by a set of new goals which are the new Antecedents (if any).

Note that Simple Rules need not have Antecedents, in which case their application is said to ``discharge'' a goal: the goal is replaced by an empty set of goals. For example:-

    a : {a}

could match and discharge the goal

    percy : {percy}

Rewrite Rules

A Rewrite Rule has the following syntax:-

    Rewrite_Rule   ::= Antecedents => Rewrite      |
                       Rewrite

    Rewrite        ::= Formula == Formula

An example of a rewrite rule is:-

    not(s = {}) 
   => 
    max({max(s),x}) == max(s\/{x})

This rule states, in effect, that, if not(s = {}) can be proved, any sub-formula of the current goal that has the form max({max(s),x}) can be rewritten as max(s\/{x}).

The Jokers s and x can be replaced by any formula, so that applying this rule to the goal

    max({max({0}),new}) == max({0}\/{new})

has the effect of applying the rule

    not({0} = {}) 
   => 
    max({max({0}),new}) == max({0}\/{new})

Rewrite rules are used for Backwards Inference, and are applied as follows:-

The left-hand side of the Rewrite is matched to any sub-formula of the current goal by substituting a formula for each Joker which makes the Consequent identical to the goal. If no such match can be found, the rule cannot be applied.
If the match is successful, the same substitution of formulae for Jokers is applied to the right-hand side of the Rewrite, and to Antecedents (if any).
The current goal is replaced by a set of goals which comprises:-

the new goal resulting from applying the Rewrite to the matched sub-formula of the current goal; and
the new Antecedents (if any).

Note that a Rewrite Rule need not have Antecedents.

Forward Rules

A Forward Rule has the following syntax:-

    Forward_Rule ::= Antecedents => Consequent

An example of a Forward Rule is :-

    not(a:T) &
    a:(S\/T)
   =>
    a:S

This rule states, in effect, that, if it is known that not(a:T) and that a:(S\/T), then it is also known that a:S.

The Jokers a, S and T can be replaced by any formula, so that applying this rule to the hypotheses

    not(percy:STAFF) & 
    percy:(CUSTOMER\/STAFF)

has the effect of applying the rule

    not(percy:STAFF) &
    percy:(CUSTOMER\/STAFF)
   =>
    percy:CUSTOMER

Forward rules are used for Forwards Inference, which is used every time a new hypothesis is introduced into the set of hypotheses.

Forwards rules are applied as follows:-

The Antecedents are matched to the current set of hypotheses by substituting a formula for each Joker which makes each Antecedent identical to one of the hypotheses. If no complete match can be found, the rule cannot be applied.
If the match is successful, the same substitution of formulae for Jokers is applied to the Consequent.
The new consequent is added to the current set of hypotheses.

Note that a Forwards Rule must always have Antecedents.

Backward Rules

Backwards Rules are Simple Rules or Rewrite Rules.

Pattern Matching

The presence of jokers in formulae allow pattern matching to take place. A formula f matches a formula g if a substitution S of formulae for the jokers of f can be found such that [S]f is identical to g.

For example, matching the formula

    age(p):T

to the formula

    age(percy) : 0..120

is achieved using the substitution

    p , T := percy , (0..120)

Special care must be taken with the matching to comma-separated lists. The comma operator is treated just like other left-associative infix operators. So the formula {p} can match the formula {1,2,3} with substitution

    p := 1,2,3

whereas {P,p} would match as

    P , p := (1,2) , 3

Guards

Guards are a special kind of Antecedent for backwards rules that are evaluated in a different way during proof construction. The proof mechanism prevents rules from being applied if the guards do not evaluate to true.

Guards also provide a means of making inference rules more generic. Their syntax is as follows:

    Guards     ::= Guards & Guard                                     |
                   Guard

    Guard      ::= "binhyp" ( Formula )                               |
                   "bnum" ( Formula )                                 |
                   "bident" ( Formula )                               |
                   "bstring" ( Formula )                              |
                   "btest" ( Number Comparison Number )               |
                   "bsearch" ( Formula , ( Formula_List ) , Formula ) |
                   "breade" ( Formula , Formula_List , Formula )

    Comparison ::=  <  |  <=  |  >  |  >=  |  =  |  /=

In this context, a Number is any Natural number less than 2^32. A Formula_List is comma (or in some cases ``&'', ``or'' or ``;'') separated list of Formulae.

A brief explanation of these guards is as follows:-

binhyp(x): succeeds if there is a hypothesis which matches x. For example, application of the following the simple rule
btest( x > y ): succeeds if x and y are valid numbers, and x is greater than y (and similarly for the other comparison operators). For example:-
bsearch(x,(l),r): succeeds if the formula x matches a formula in the list l, and r is the list l with the matched formula removed. The list can be separated by commas, ``&'' or ``or''.
breade(f,l,x): displays the list of formulae l on the screen according to the format given in the quoted string f, and succeeds if x matches the response typed by the user.
bident(x): succeeds if x is a valid identifier (a string of length greater than 1 comprising upper or lower-case letters, digits and the underscore character, and containing at least one letter).
bnum(x): succeeds if x is a valid number (a Natural number less than 2^32).
bstring(x): succeeds if x is a valid quoted string (any character string enclosed in double quotes).

Note the subtle difference in the syntax for bsearch and breade. The second argument of bsearch must be a list enclosed in brackets, whereas the list in breade does not, giving rise, in effect, to a variable number of arguments (rather like the printf function in C). The x thus refers, in fact, to the last argument.

Theories

A Theory is a container for inference rules. A forward theory contains forward rules, and a backward theory contains backwards rules.

    Theory      ::= THEORY Theory_Name IS Rule_List END

    Theory_Name ::= Identifier 

    Rule_List   ::= Rule_List ; Inference_Rule  |
                    Inference_Rule

In the Proof Method files presented by the user to the InterProver, backwards rules and forwards rules are presented in two theories, usually called UsersTheory and FwdUsersTheory respectively. There is no reason, however, why users should not present any number of theories with others names, as long as the appropriate tactics are also amended.

The order of rules in a theory is significant. (See Ordering Rules in Theories below for a discussion of this.)

Tactics

B-TL provides a very simple tactic language which guides proof construction. The language describes sequencing and iteration of theory applications, and names some basic atomic tactics. The syntax is as follows:-

    Tactic        ::= Atomic_Tactic    |
                      Tactic ; Tactic  |
                      Tactic~

    Atomic_Tactic ::= DED  |  GEN  |  SUB  |  HYP  |  FEQL  |  Theory_Name

The semicolon indicated sequencing of actions, and the tilda indicates repetition. The following is an example of a tactic:-

    ( Theory1 ; DED ) ~ ; Theory2~

which says, in effect:-

First attempt to apply any rule from theory Theory1, then apply the special tactic DED.
Repeat 1 until no more rules apply.
Then repeatedly apply any rules from Theory2 until no more apply.

In the Proof Method files used by the InterProver, two tactics are named in the USETAC clause (see section on InterProver). The first is the tactic to be used for backwards inference, and the second is for forwards inference.

By default, these two tactics are presented as:-

    (UsersTheory~),
 
    (FwdUsersTheory~/*;FEQL~*/)

and the user is expected to present backwards rules in a theory called UsersTheory and forwards rules in FwdUsersTheory.

Note that the application of the special tactic FEQL is commented out by the annotation marks /* and */. It is placed there to remind users that a frequently desired modification of the forward tactic is to include the ``forwards equality'' tactic. In some applications, this modification helps to push proofs through, often without providing additional rules. It is left out of the default for efficiency reasons.

The special tactics are described as follows:-

DED: The deduction tactic, DED, acts on goals of the form
GEN: The generalisation tactic, GEN, acts on goals of the form
SUB: The substitution tactic, SUB, acts on goals with contain sub-formulae of the form
HYP: The ``hypothesis'' tactic, HYP, can act in a number of ways. Suppose the current goal is Q:-
FEQL: The ``forward equality'' tactic, FEQL is a forward tactic which generates new hypotheses from the set of current hypotheses by calculating the transitive closure of equality.

Proof Construction

Proofs are constructed in the context of:-

A set of goals, one of which is the current goal.
A set of current hypotheses.
A normal tactic, with a current position.
A forwards tactic, with a current position.
A set of theories.

At the start of proof:-

A single goal exists in the set of goals, which is selected as the current goal.
The set of current hypotheses is empty.
Normal and forwards tactic positions are pointing at the first theory or special tactic.

As proof proceeds, the set of current hypotheses, the set of goals, the choice of current goal, and the tactic positions are manipulated as follows:-

An attempt is made to find a rule from the theory named at the current current normal tactic position which matches the current goal.
If a matching backwards rule is found, it is applied, which may result in the addition of hypotheses to the set of current hypotheses, and to manipulation of the set of goals, as described in the section describing backwards inference.
If the set of goals is now empty, proof is concluded with success.
If new hypotheses are introduced, forward inference is applied as described below.
The normal tactic position is incremented, taking repetition into account.
If the end of the normal tactic is reached, proof terminates unsuccessfully.
A new current goal is selected (usually a child of the last current goal).
Proof construction is repeated from 1.

The forward inference process referenced in step 4 above is as follows:-

An attempt is made to find a rule from the theory (or special tactic) named at the current forwards tactic position which matches formulae from the set of current hypotheses.
If a matching forwards rule is found, it is applied, which may result in the addition of hypotheses to the set of current hypotheses.
The forwards tactic position is incremented, taking repetition into account.
Forward inference is repeated from 1.
When the end of the forwards tactic is reached, forwards inference terminates.

Guidelines for Proof

The following notes are intended to guide the B-Toolkit in constructing theories for use with the InterProver.

Ordering Rules in Theories

When applying rules from a theory, rules are matched in strict biblical order: the last first, and the first last. This allows a further aspect of control over which rules are applied: a rule is applied only if all other rules below it in the theory have not matched.

For example, consider the following theory:-

    THEORY max IS
        max({p}) == p
    ;
        max({max(P)}\/Q) == max(P\/Q)
    ;
        max({P,p}) == maxel({P,p},0)
    ;
        maxel({p},q) == p
    ;
        btest(q>p) 
       =>
        maxel({p},q) == p
    ;
        maxel({P,p},q) == maxel({P},p)
    ;
        btest(q>p) 
       =>
        maxel({P,p},q) == maxel({P},q)
    END

The last rule is attempted first. This rule is guarded by a btest. If this fails, then the next rule above is attempted.

The rewrite in the next rule has an identical left-hand side, so the rule will match exactly when the bottom rule does. This time, however, there is no guard, but we know from the failure of the rule below that it will only apply when q<=p.

Together, these last two rules cover all cases when there are at least two elements in the set in the first argument of maxel.

The next rule up has a rewrite with a different (more general) left-hand side. The formula {p} can match any set, including those of the form {P,p} (see Pattern Matching). But we know that, since the previous rules did not match, the only pattern that remains to be matched is the single set, in which matches a single element, and not a comma-separated list. A similar argument applies to the top rule.

Using Guards in Rewrite Rules

The use of guards is strongly advised for rewrite rules. This is because there is limited backtracking through rewrite rules: once they are applied, they cannot be unapplied through backtracking. There is a need, therefore, to have careful control over the application of rewrite rules.

The first control over the application of a rewrite rule is through pattern matching: the rule will only apply if the shape of the left-hand side of the rewrite matches a sub-formula of the current goal.

A second level of control is by judicious ordering of rewrite rules in the theory. (See Ordering Rules in Theories above.)

A third level of control is by using guards in the antecedent of the rule: if guards evaluate to false, the rule is not applied.

A better version of the rewrite rule example given above is thus:-

    binhyp(not(s = {})) 
   => 
    max({max(s),x}) == max(s\/{x})

since this only allows rewriting when it is known from the current set of hypotheses that
not(s = {}).

Backwards versus Forwards Inference

Backwards inference is goal-oriented, in that rules matched against the current goal. It is therefore inherently more efficient than forwards inference, which is not goal-directed, since it blindly propagates knowledge from the hypotheses.

It is therefore recommended that simple rules and rewrite rules are used in preference to forwards rules where ever possible.

Supplying Rules for Animation

For the purposes of Animation of AMN specifications in the B-Toolkit, a theory file can be supplied containing only guarded or unguarded rewrite rules. Other kinds of rules would interfere with the animation mechanism. (See section on the Animator entitled Providing More Rewrite Rules.)

Running Out of Memory

When conducting really large proofs, it is possible for the B-Platform to run out of memory. If this occurs, an error message is displayed in the AutoProver or InterProver panel, and the proof session is aborted. Hopefully, this situation will not arise, as memory is allocated through the malloc utility; more memory may be freed by shutting down other processes, or increasing the swap space of the machine on which it is running - see your System Administrator.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo