A Short Tutorial to Princess

Try with: Web Interface Java Webstart

We outline some of the Princess functionality and use cases:

Presburger Arithmetic and Quantifier Elimination

To illustrate what can be expressed using Presburger arithmetic, we first look at a very simple puzzle (found here):

"My grandson is about as many days as my son is weeks, and my grandson is as many months as I am in years. My grandson, my son and I together are 140 years. Can you tell me my age in years?"

Solving this puzzle boils down to finding the (integer) solutions of a system of linear equations, which is a problem that can be written in Presburger arithmetic. We can first check the existence of solutions:
\exists int grandson_years, son_years, my_years,
            grandson_months, son_weeks, grandson_days; (
  grandson_days = grandson_months * 4 * 7 &
  grandson_months = grandson_years * 12 &
  son_weeks = son_years * 12 * 4 &
  grandson_days = son_weeks &
  grandson_months = my_years &
  grandson_years + son_years + my_years = 140
)
To feed this problem into Princess, we need to wrap the statement \problem{ ... } around the formula. The Princess prover can then simply be web-started and be run on the formula, which results in something like this. Princess confirms that the system of equations is solvable:
No countermodel exists, formula is valid
Of course, we would also like to know the answer to the puzzle! To determine and output the age of the storyteller, we need to remove the quantifier for the variable my_years and declare it as an implicitly existentially quantified constant instead:
\existentialConstants {
  int my_years;
}

\problem {
  \exists int grandson_years, son_years,
              grandson_months, son_weeks, grandson_days; (
    grandson_days = grandson_months * 4 * 7 &
    grandson_months = grandson_years * 12 &
    son_weeks = son_years * 12 * 4 &
    grandson_days = son_weeks &
    grandson_months = my_years &
    grandson_years + son_years + my_years = 140
  )
}
Now, Princess will also provide us a solution for my_years, namely 84. This solution is given as a conjunction of equations over the existential constants (in our example, there is only a single constant my_years):
Formula is valid, satisfying assignment for the existential constants is:
my_years = 84

We might want to know whether 84 is the only solution of the puzzle, or whether the storyteller could be younger or older than this. The first way to achieve that is to add the option +mostGeneralConstraint to the "Options" text field in the bottom of the Princess window. This option makes Princess search for all solutions of the formula, instead of stopping after she has found the first one. This is realised by  means of quantifier elimination. For our example, the output will be the following:

Formula is valid, resulting most-general constraint:
my_years = 84

Concrete witness:
my_years = 84
This means that 84 is the only solution to the puzzle.

Note: The option +mostGeneralConstraint should be used with care if also uninterpreted predicates are involved, as described below, because it can easily lead to non-termination.

A second way to search for further solutions (which sometimes can be more efficient) is to simply add a disequation or inequality like my_years < 84 to the problem:

\existentialConstants {
  int my_years;
}

\problem {
  \exists int grandson_years, son_years,
              grandson_months, son_weeks, grandson_days; (
    grandson_days = grandson_months * 4 * 7 &
    grandson_months = grandson_years * 12 &
    son_weeks = son_years * 12 * 4 &
    grandson_days = son_weeks &
    grandson_months = my_years &
    grandson_years + son_years + my_years = 140
  )
  &
  my_years < 84
}

This time, Princess tells us that it was not able to solve the problem (do not forget to remove the option +mostGeneralConstraint again):

Formula is invalid, found a countermodel:
true
Because Princess actually is complete for problems in Presburger arithmetic, she is able to tell us that no solution exists.

Basic Uninterpreted Predicates

Princess can also handle problems containing uninterpreted predicates, which makes the accepted language strictly more expressive than Presburger arithmetic (in fact, too powerful to allow complete calculi; intuitively, Princess can prove only those valid formulae for which no induction is needed). As a simple example, we could introduce a binary predicate divides (which is not part of Presburger arithmetic) and add axioms that describe the concept of divisibility:

\predicates {
  divides(int, int);
}

\problem {
  //
  // Axioms
  //
     \forall int x; divides(x, x)
  -> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))
  ->
  //
  // Problem to be proven
  //
     divides(7, 49)
}
Run on this example, Princess will again tell us that it has found a proof of validity:
Formula is valid, resulting constraint:
true

By adding existential constants, we can use Princess for factorising numbers or for computing common divisors of two numbers (not that this would be particularly efficient, however):

\existentialConstants {
  int A, B;
}

\predicates {
  divides(int, int);
}

\problem {
     \forall int x; divides(x, x)
  -> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))
  ->
     divides(A, 51) & A < 51 & A > 1 &
     divides(B, 42) & divides(B, 49) & B > 1
}
The result is something like:
Formula is valid, resulting constraint:
B = 7 & A = 17

Concrete witness:
B = 7 & A = 17

Somewhat more intricate, we can also express that we are interested only in greatest common divisors of two numbers:

divides(A, 42) & divides(A, 49) &
\forall int x; (divides(x, 42) & divides(x, 49) & x > 1 -> x <= A)
Interestingly, this property is not provable with the given axioms for the predicate divides. This is because the two axioms only tell for which arguments divides holds, but not for which arguments it does not hold. Consequently, Princess is able to derive that 7 is a common divisor of 42 and 49, but not that no larger number is a common divisor as well.

Note: Princess will not terminate when run on the example and has to be stopped manually.

We need to add a third axiom stating that 0 is the only element of the interval (-x, x) that is divided by x:

\existentialConstants {
  int A;
}

\predicates {
  divides(int, int);
}

\problem {
     \forall int x; divides(x, x)
  -> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))
  -> \forall int x, y; (divides(x, y) & y < x & y > -x -> y = 0)
  ->
     divides(A, 42) & divides(A, 49) &
     \forall int x; (divides(x, 42) & divides(x, 49) & x > 1 -> x <= A)
}
Now, Princess is able to derive a solution:
Formula is valid, resulting constraint:
A = 7

Concrete witness:
A = 7

Craig Interpolation

Besides reasoning about the validity/satisfiability of problems, Princess is also able to extract Craig Interpolants from valid formulae. This functionality is described in the following documents: paper 1 (JAR), paper 2 (VMCAI). Interpolants summarise the information flow that takes place when proving the validity of a formula, and are useful for a variety of applications related to program verification, for instance approximative image computation and the construction/refinement of abstractions.

In order to compute interpolants, a formula first has to be partitioned into a number of disjuncts. The individual parts are marked and labelled using the keyword \part; the labels can then be used to formulate a sequence of interpolation problems with the help of the keyword \interpolant. For instance, in the following problem two disjuncts left and right have been marked, and we request the computation of an interpolant for the implication left -> right: 

\functions {
  int c, d;
}

\problem {
  \part[left] (c > d & d > 0)
->
  \part[right] c > 0
}

\interpolant {left; right}
The output of Princess for this problem is something like: 
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
c >= 2
The interpolant c >= 2 has the property that left -> c >= 2 and c >= 2 -> right, and is a formula over the common vocabulary of left and right; the interpolant can thus be seen as an intermediate formula between left and right.

It is possible to have more than two \parts in a problem, and to use multiple \interpolant statements. Consider the following program with variables ranging over unbounded integers: 

if (a == 2*x && a >= 0) {    // point (1)
  b = a / 2;                 // point (2)
  c = 3*b + 1;               // point (3)
  assert (c > a);
}
In order to verify the assertion, the program is translated into a formula in Presburger arithmetic. Note that b = a / 2 is converted into a conjunction of two inequalities; also, we introduce labels for each statement in the program: 
\functions {
   int x, a, b, c;
}

\problem {
  \part[cond]          (a = 2*x & a >= 0) &
  \part[stmt1]         (2*b <= a & 2*b >= a - 1) &
  \part[stmt2]         c = 3*b + 1
                       ->
  \part[assert]        c > a
}

\interpolant {cond; stmt1, stmt2, assert}
\interpolant {cond, stmt1; stmt2, assert}
\interpolant {cond, stmt1, stmt2; assert}
In each \interpolant clause, the labels left of the semicolon specify the left partition, the labels right of the semicolon the right partition. Given this input, Princess now computes three interpolants, for the three different partitionings that were specified: 
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
a >= 3 | (a >= 0 & \exists int v0; 2 * v0 = a)
3 * b >= a
c - a >= 1

The three interpolants represent invariants that hold true at different points of the original program: the first interpolants holds immediately after the if-condition (at point (1)), the second interpolants holds at point (2) after the first assignment, and the third interpolant at point (3) in front of the assertion.

What is going on internally in Princess

  1. The input problem is transformed to disjunctive normalform; in the example, something like !cond | !stmt1 | !stmt2 | assert.
  2. It is checked that all the \part annotations are in front of top-level disjuncts. If they are not, e.g., you end up with a disjunct (\part[X] foo) & (\part[Y] bar), an error message will be raised.
  3. The \part annotations are stripped away, and it is checked/proven whether the resulting formula/disjunction is valid or invalid.
  4. If it was possible to prove that the input formula is valid, the stated interpolation problems are considered, each of which specifies a partitioning of the disjuncts that were determined in step 1. I.e. for a clause \interpolant {A1, ..., An; B1, ..., Bm}, and assuming that A1, ..., An, B1, ..., Bm are the disjuncts in step 1, a formula I is computed that satisfies the implication !A1 & ... & !An -> I and !A1 & ... & !Bm -> !I. I is computed in such a way that it only contains symbols (constants, functions, predicates) that are common to the left partition A1, ..., An and the right partition B1, ..., Bm.

Because all the interpolants are generated from the same proof (extracted in step 3), it is also guaranteed that the interpolants satisfy the "chaining property," in case the input problem and \interpolant clauses specify a chain. That means, if we have an interpolation problem of the form 

\problem {
  \part[p1] f1
&
  \part[p2] f2
&
  // ...
&
  \part[pn] fn
->
  false
}

\interpolant { p1; p2, ..., p(n-1), pn }
\interpolant { p1, p2; ..., p(n-1), pn }
// ...
\interpolant { p1, p2, ..., p(n-1); pn }
then the generated interpolants I1, I2, ..., I(n-1) satisfy the implications

Uninterpreted Functions and Triggers

In addition to uninterpreted predicates, it is also possible to use uninterpreted functions for formulating problems in Princess. The Princess method to handle functions is described in an LPAR paper. To illustrate the use of functions, we consider another riddle (taken from this page):

Here's a variation on a famous puzzle by Lewis Carroll, who wrote Alice's Adventures in Wonderland.
"A group of 100 soldiers suffered the following injuries in a battle: 70 soldiers lost an eye, 75 lost an ear, 85 lost a leg, and 80 lost an arm. What is the minimum number of soldiers who must have lost all 4?"

This puzzle could be formalised in the Princess syntax by declaring 16 constant symbols:

This corresponds to partitioning the set of 100 soldiers into 16 disjoint subsets. The conditions of the puzzles can then be captured using a set of equations and inequalities.

Since the declaration of so many constants is a bit cumbersome, instead we can use an uninterpreted function with four integer arguments: 

\functions {
  int inj(int,  // lost an eye?
          int,  // lost an ear?
          int,  // lost a leg?
          int   // lost an arm?
         );
}
Instead of a constant n0000, we can now simply write inj(0,0,0,0), etc.

The riddle can then be translated to a conjunction of equations, together with a universally quantified formula that ensures that the function inj represents non-negative values. Since we are interested in a lower bound of the value inj(1,1,1,1) (the number of soldiers who lost all four), we additionally introduce an existential constant MinNum and add the inequality inj(1,1,1,1) >= MinNum as a conclusion supposed to follow from the conditions of the riddle:

\existentialConstants {
  int MinNum;
}

\functions {
  int inj(int, int, int, int);
}

\problem {
// 100 soldiers altogether
  inj(0,0,0,0) + inj(0,0,0,1) + inj(0,0,1,0) + inj(0,0,1,1) +
  inj(0,1,0,0) + inj(0,1,0,1) + inj(0,1,1,0) + inj(0,1,1,1) +
  inj(1,0,0,0) + inj(1,0,0,1) + inj(1,0,1,0) + inj(1,0,1,1) +
  inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 100
&
// 70 soldiers lost an eye
  inj(1,0,0,0) + inj(1,0,0,1) + inj(1,0,1,0) + inj(1,0,1,1) +
  inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 70
&
// 75 soldiers lost an ear
  inj(0,1,0,0) + inj(0,1,0,1) + inj(0,1,1,0) + inj(0,1,1,1) +
  inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 75
&
// 85 soldiers lost a leg
  inj(0,0,1,0) + inj(0,0,1,1) + inj(0,1,1,0) + inj(0,1,1,1) +
  inj(1,0,1,0) + inj(1,0,1,1) + inj(1,1,1,0) + inj(1,1,1,1) = 85
&  
// 80 soldiers lost an arm
  inj(0,0,0,1) + inj(0,0,1,1) + inj(0,1,0,1) + inj(0,1,1,1) +
  inj(1,0,0,1) + inj(1,0,1,1) + inj(1,1,0,1) + inj(1,1,1,1) = 80
&
// inj is non-negative
  \forall int x1, x2, x3, x4; inj(x1, x2, x3, x4) >= 0
->
// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4
  inj(1, 1, 1, 1) >= MinNum
}
When running Princess on this input, she will check whether any value MinNum exists such that the stated implication holds, for any valuation of the function inj that satisfies the given conditions. Indeed, such values can be found: 
Proving ...

Formula is valid, resulting constraint:
10 >= MinNum

Concrete witness:
MinNum = 10
This means that any MinNum <= 10 (and in particular 10) is a lower bound of inj(1,1,1,1); at least 10 soldiers must have lost all four.

Tightening the lower bound

Though we now know that 10 is a lower bound, we don't know yet whether 10 is the greatest lower bound (that was asked for in the puzzle). There are different ways to check whether the bound 10 is tight; most simply, we can add an additional inequality to the Princess input, forcing the prover to search for values MinNum > 10:

[...]

\problem {
  [...]
->
// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4
  inj(1, 1, 1, 1) >= MinNum & MinNum > 10
}
Princess won't be able to find any such values, indicating that 10 is indeed a tight bound. However, since Princess is not able to recognise that the search for values MinNum > 10 is futile, proof search won't terminate for the input at all and has to be stopped manually after some while (by pressing the Stop button in the GUI).

A more elegant way to find the greatest lower bound is to tell Princess to search for the most general constraint satisfying the original problem input (in the same way as it was done in the first example on this page). For this, we have to ensure termination of proof search, and remove the cause of non-termination that occurred in the first attempt (when adding the inequality MinNum > 10): the totality axiom that Princess implicitly generated for the function symbol inj. Intuitively, such totality axioms have the form \forall int x1, x2, x3, x4; \exists int y; inj(x1, x2, x3, x4) = y, and the somewhat unfortunate property that they can be instantiated indefinitely and thus prevent proof search from terminating. At the same time, for many applications (in particular for our riddle) the totality property of functions is not required. More details are given in this paper, and in the next section on this page.

To generate the most general constraint on MinNum for the riddle, perform the following steps:

After this, Princess will create output similar to the following: 
Proving ...

Formula is valid, resulting most-general constraint:
10 >= MinNum

Concrete witness:
MinNum = 10

Types of uninterpreted functions in Princess

Functions are internally encoded as relations, in combination with axioms expressing functionality and totality. Consequently, functions can be declared in a number of ways:
In many cases, the totality axiom is not needed for proving the validity of a problem. At the same time, the totality axiom is rather expensive to handle (for Princess), so that it is often a good idea to first declare all functions as partial, and only later introduce total functions as needed.

A computational encoding of the riddle

The first encoding of the soldier riddle (using the function inj) was still not exactly elegant, since we had to spell out a set of long equations by hand. The equations corresponding to the riddle can also be written in a more symbolic way, by introducing further uninterpreted functions. To simplify things, we now encode the four integer arguments of the function inj (each ranging over the set {0, 1}, i.e., encoding a single bit) as a single integer ranging over {0, 1, ..., 15}. It is then easy to compute the number of all soldiers (the sum inj(0) + inj(1) + ... + inj(15)) using two axioms and a further uninterpreted function sum. We use partial functions at this point, since totality is not needed in the formalisation: 

\functions {
  \partial int inj(int);
  \partial int sum(int);
}

\problem {
  sum(0) = 0
&
  \forall int x; {sum(x)} (x>0 -> sum(x) = sum(x-1) + inj(x-1))
&
  sum(16) = 100        // 100 soldiers altogether

&
  [...]
}
Triggers: Note the expression {sum(x)} used in the second axiom: this expression is a trigger and tells Princess in which way the axiom is supposed to be handled. Generally, triggers consist of a single or multiple expressions (normally sub-expressions in the body of the quantified formula) that contain all quantified variables. Princess uses the term sum(x) as a pattern; whenever an instance sum(t) of the pattern occurs during proof search, she will create a ground instance of the quantified axiom in which x has been replaced with the term t. This will lead to the sum sum(16) incrementally being computed from sum(15) and inj(15), then sum(14), and so on, in the same way as a recursive procedure is evaluated.

The other conditions of the riddle can be captured in a similar way, although slightly more complicated axioms are needed. In particular, we have to define a binary function bit for extracting individual bits of an integer. The resulting formalisation is shown in the next listing:

/*
   Solve with options "-generateTriggers=all +mostGeneralConstraint"
 */

\existentialConstants {
  int MinNum;
}

\functions {
  \partial int inj(int);
  \partial int sum(int);
  \partial int pSum(int, int);
  \partial int bit(int, int);
}

\problem {
// Recursive extraction of individual bits in an integer number
  \forall int x1, x2, b; {bit(2*x1 + x2, b)} (
     x2 >= 0 & x2 < 2 ->
        (b > 0 -> bit(2*x1 + x2, b) = bit(x1, b-1)) &
        (b = 0 -> bit(2*x1 + x2, b) = x2)
  )

// Recursive computation of the sum "inj(0) + inj(1) + ... + inj(15)"
&
  sum(0) = 0
&
  \forall int x; {sum(x)} (x>0 -> sum(x) = sum(x-1) + inj(x-1))

// Recursive computation of the sum of the inj(i), for those i where bit b is set
&
  \forall int b; pSum(0, b) = 0
&
  \forall int x, b; {pSum(x, b)} (
     x>0 -> pSum(x, b) = pSum(x-1, b) + (\if (bit(x-1, b) = 1) \then (inj(x-1)) \else (0)))

& sum(16) = 100        // 100 soldiers altogether
& pSum(16, 0) = 70     // 70 soldiers lost an eye
& pSum(16, 1) = 75     // 75 soldiers lost an ear
& pSum(16, 2) = 85     // 85 soldiers lost a leg
& pSum(16, 3) = 80     // 80 soldiers lost an arm

&
// inj is non-negative
  \forall int x; inj(x) >= 0

->
// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4
  inj(15) >= MinNum
}
It can be observed that most, but not all of the quantified axioms contain hand-written triggers. For the remaining axioms, we can rely on the fact that Princess will automatically generate triggers if none are provided. This functionality is controlled by the option -generateTriggers: