Introduction to the Theory Language

The mathematical rules used by the prover are written in the so-called “theory language”. Without getting into the details of this language, which is similar to PROLOG, the following sections expose the fundamental notions that may be employed to use the theory language for the purpose of defining mathematical rules.

What is a wildcard?

A wildcard is a value that can take any value (literal, expression, etc.) If it is assigned a value, then it is said to be instantiated.

The sole mechanism to represent a variable is the wildcard. A wildcard is denoted as a single (latin) alphabet letter: one cannot have more that 52 wildcards inside a rule (considering both uppercase and lowercase letters).

For instance, the expression

a + bb*cc - d

contains wildcards a and d and literals bb and cc.

Wildcards a and d may be instantiated with ee+1 and 3, respectively. We then obtain the expression:

ee + 1 + bb*cc - 3

What is a formula?

A formula is an expression that is built out of

• wildcards,

• literals and numbers

• logical connectors:

  • conjunction : &

  • disjunction : or

  • implication : =>

  • equivalence : <=>

  • negation : not

• quantifications:

  • universal quantification : !

  • existential quantification : #

• equality : =,

• set membership : :,

• set inclusion : <:

• operators to combine arithmetic, set, boolean, relational, functional and sequence expressions of the B language (see [2] ), obeying the syntax of the B language.

For instance,

0=<aa & 0=<bb => 0<=aa*bb
a=TRUE or b=TRUE => a : BOOL

are syntactically correct formulas.

In summary, the language for formulas is the language of B expressions extended with wildcards.

Matching Formulas

A formula f is said to match a formula g, if it is possible to obtain f by substituting, in g, all the occurences of the same wildcards with some formulas . Recall that a wildcard is an atomic formula composed of a single letter . A wildcard is thus a “formula variable”. For instance the following formula g:

aa + (bb/ee - (cc + dd)*aa) - bb/ee

matches the following formula f:

x + (y - z*x) - y

An assignment of formulas to wildcards is called a filter. A filter is thus a partial function from wildcards to formulas. Applying a filter to a formula g consists in replacing each wildcard occurence in g, that belongs to the domain of the filter, by the corresponding formula. In summary, a formula f matches a formula g if there is a filter such that the application of that filter to g yields f. In the case of the previous matching, we have the following filter:

{ x |-> aa, y |-> bb/ee, z |-> cc + dd }

What is a rule?

A rule is a formula with the following form A => B. A is called the antecedent of the rule, B is called the consequent of the rule. A and B may be conjunctions of predicates. A may be omitted, in that case, the rule is said to be atomic. A rule may be:

• inductive (backward)

If the current goal is B, then to prove B it is sufficient to prove A. A is supposed to be simpler, or easier to prove, than B. For instance, with the rule

x = FALSE => not(x = TRUE)

the goal

not (bool(0 <= aa*bb) = TRUE)

is proved if the derived goal

bool(0 <= aa*bb) = FALSE

is proved. Similarly, the atomic rule

not (BOOL = {})

is applied to prove immediately the goal with the same form.

• deductive (forward)

If the antecedent A has the following form:

A1 & A2 &... & An

and if A1 is an hypothesis that has just been generated, and if

A2 & ... & An

are in the hypothesis stack then instances of predicates in the conjunction B are generated and, if they do not appear in the hypothesis stack, are pushed onto that stack. For instance, with the rule:

not(a=b) & a=c => not(b=c)

If the hypothesis not(xx = 3) has just been generated, and the hypothesis xx = aa * bb – cc is in the hypothesis stack, then the hypothesis not(3=aa*bb-cc) is generated.

• rewrite

In this kind of rules, B has the form C == D. If A is satisfied, then C is rewritten to D. This kind of rules only applies to subformulas of the current goal, or on the current goal itself. For instance, the rule SimplifyIntMaxXY.3:

btest(p<=q)                    /* If p and q are integers */
=>                                 /* such that p <= q */
max({p}/{q}) == q        /* then max({p}/{q}) rewrites to p *

applies to the goal

0 <= max({3}/{5}) - min(1..4)

and rewrites it to

0 <= 5 - min(1..4)

The rules contain wildcards, whereas hypothesis do not.

Application of a rule to a formula

To realize formal proofs, inference rules are applied. This section explains what is meant by applying an inference rule to a formula. The result of the application of a rule r to a formula f yields other formulas that are called the successors of f. The set of successors may be empty. Also note that a rule is not always applicable to a formula. When a rule r is applied to a formula f, r is said to discharge f and produces a number of formulas.

We are now going to state in which conditions a rule is applicable to a formula and, if when it is, define the result of this application. Recall that a rule has the following general form:

a1 & a2 & ... * an => c

where a1, a2,… , an are called the rule antecedents, and c is the rule consequent. To apply a rule to a formula, one must consider two cases, depending on the nature of the consequent c.

Deduction rule

When the consequent of the rule does not have the form g == d, then the rule is a deduction rule. For instance, the following is a deduction rule:

x < z & y < z => x+y < 2*z

A deduction rule is applicable to a formula f when f matches the consequent of r, yielding a filter. The result of the application of r to f is then the application of this filter to the different antecedents of r. This result may be empty when the rule has no antecedent. For instance, the application of the previous rule to the following formula:

aa+bb+cc < 2*(cc+dd)

produces the two following formulas:

aa+bb < cc+dd
cc < cc+dd

Note that the filter resulting from this matching is due to the left-recursive nature of the parser. Indeed, aa+bb+cc matches x + y with x matched to aa+bb and y matched to cc.

So the rule

aa+y

matches aa+bb but not aa+bb+cc, as it is parsed as (aa+bb) + cc.

Rewrite rule

When the consequent c of the rule has the form g == d, then the rule is called a rewrite rule. In such rules, formula g and d are called the left hand side and theright hand side. For instance, the following is a rewrite rule (without antecedent):

x*(y+z) == x*y + x*z

Such rule is applicable to a formula f if there exists a sub-formula h of f such that h matches the left-hand side of the consequent of r, yielding a filter. The result of the application of r to f corresponds first, as in the previous case, to the application of the filter to the antecedents of r, if there is any. The result also contains the formula obtained by replacing, in f, the sub-formula h by the application of the filter to the right-and side of the consequent of r. Consequently, the application of the previous rule to the formula

aa + bb + cc*(ee+ff) < cc + dd

produces the following formula:

aa + bb + (cc*ee + cc*ff) < cc + dd

If several subformulas match the left-hand side of the consequent, the “rightmost” sub-formula is chosen. For instance, when the rule

a+b == b+a

is applied to formula

aa+bb+cc = cc+bb+aa

four subformulas match the left hand side, namely:

aa+bb
aa+bb+cc
cc+bb
cc+bb+aa

The selected sub-formula is thus cc+bb+aa. The rewrite rule results in the following formula:

aa+bb+cc = aa+(cc+bb)

What is a theory?

A theory is a group of rules, written in the theory language. Two consecutive rules are separated by a ‘;’ (semi-colon). The rules are (implicitly) named t.n, where

• t is the name of the theory

• n : is the position of the rule in the theory, the first position being numbered 1.

Example :

THEORY th1 IS
binhyp(a: B) & /* Rule th1.1 */
binhyp(B<: C)
=>
a: C;

btest(0 <= -t) /* Rule th1.2 */
=>
0<=t**2 - 4*t + 1
END

The prover first tries to apply rules with a higher index before a rule with a lower index (from the bottom to the top of the theory). For instance, when using the command ar(th1) (see [3]), the prover always tries to apply rule th1.2 before th1.1. In the case of this command, a rule th1.n only applies when no rule th1.m (such that n < m) applies. When a rule has been applied, the prover repeats its search from the last rule of the theory.

Proof

Proof of a formula

Given a set of rules, a formula f is said to be formally proved under this set of rules, when the repeated applications of these rules to the initial formula f and its successors, and the successors thereof, and so forth, results in an empty set. Equivalently, the formula f is proved under a set of rules when f and all its descendants are discharged by said these rules.

The initial formula and its descendants are called the goals of the proof. The initial formula is the initial goal, and its descendants are intermediate goals that appear during the course of the proof. By definition, all the goals are proved at the end of the proof.

This definition leaves space to some non-determinism, as we specify neither the order in which the intermediate goals are proved, nor the order in which the rules are chosen to discharge a given goal.

For instance, given the following rules:

x < z & x < z => x+y < 2*z
a-a == 0
x < x+1
0 < x+1

the goal is the following formula:

aa + (bb-bb) < 2*(aa+1)

The first rule may be used to discharge the initial goal, producing two intermediate goals:

aa < aa+1 bb-bb < aa+1

The first goal is discharged with the third rule, without creating any new goal. The second intermediate goal still needs to be proved. It is easy to see that can be done by discharging the second and then the fourth rule. Since neither applications produce new goals, we reach the point where no goal is left to be proved. The initial goal is then formally proved under the enuntiated set of rules.

Special case of conjunctive formulas

When a goal has the form:

f1 & f2 & ... & fn

the proof of this goal is replaced by the proof of each formula f1, f2, … fn, that become new intermediate goals.