# Soundness Prover

## Introduction

This is a short manual for the proof of concept implementation of the soundness prover of [vW08]. You can find its web interface here. Please note that this is an experimental tool and as such does not guarantee anything. Of course, questions and comments are welcome.

## Syntax

The soundness prover uses a very basic syntax. See section Examples below for an illustration.
 Identifiers Any alphanumerical string (including underscores) that is not a keyword (i.e. not one of false, true, semantics, relation, axioms, exists or forall).

Terms are made from variables and function applications:
 Variables Just an identifier. For example, x, x2, f, 0 are all variables. Function applications An identifier followed by zero or more comma-separated terms enclosed by parentheses. For example, f(x), c(), 0(), f(c(),g(x)) are all function applications.

Formulas:
 Boolean constants false and true Predicates Same as function application; the head symbol is considered the predicate (e.g. P(x)) Negation !f, where f is a formula Disjunction f || g, where f and g are formulas Conjunction f && g, where f and g are formulas Implication f -> g, where f and g are formulas Biimplication f <-> g, where f and g are formulas Existential Quantification , where f is a formula and x, y etc are variables Universal Quantification , where f is a formula and x, y etc are variables Parentheses (f), where f is a formula

In text boxes (i.e. Semantics and Auxiliary equalities we also allow comments. These are started with # and are ended by the end of the line in which they are used. Comments are ignored by the parser.

### Semantics

The semantics as given in the Semantics box should consist of the following two non-empty sections.

First the Structural Operational Semantics should be given. This section is started with the keyword semantics and should be followed by one or more SOS rules. A SOS rule is of the form f => p;, where f is a formula and p a predicate. Note the semicolon as last character.

Following the semantics section one needs to define the relation. This is done by writing relation(x,y) where x and y are variables. This is followed by one or more conjuncts that define the relation. Each conjunct is a formula followed by a semicolon (;). In these conjuncts free variables different from those as specified after relation are considered universally quantified. In defining the relation one can use the special predicate rel (with arity 2) to refer to the relation itself.

### (In)equalities

Inequalities are of the form t <= u or f => t <= u, where t and u are terms and f is a formula. The latter form is called a conditional inequality. Equalities are similar but use an = instead of an <=.

An inequality t < u is interpreted as the claim that rel(t,u) holds and an equality t = u is interpreted as the claim rel(t,u) && rel(u,t). When using a conditional (in)equality the claim is prepend with f ->.

## Example

Take the following specification for BPA* [Fok94]:

```semantics
# act
true => tick(act(a),a);

# alt
tick(p,a) => tick(alt(p,q),a);
tick(p,a) => tick(alt(q,p),a);
trans(p,a,p2) => trans(alt(p,q),a,p2);
trans(p,a,p2) => trans(alt(q,p),a,p2);

# seq
tick(p,a) => trans(seq(p,q),a,q);
trans(p,a,p2) => trans(seq(p,q),a,seq(p2,q));

# star
tick(p,a) => trans(star(p,q),a,star(p,q));
trans(p,a,p2) => trans(star(p,q),a,seq(p2,star(p,q)));
tick(q,a) => tick(star(p,q),a);
trans(q,a,q2) => trans(star(p,q),a,q2);

# plus
tick(p,a) => trans(plus(p,q),a,alt(plus(p,q),q));
trans(p,a,p2) => trans(plus(p,q),a,seq(p2,alt(plus(p,q),q)));

relation(x,y)
rel(y,x);
trans(x,a,x2) -> <exists y2: trans(y,a,y2) && rel(x2,y2)>;
tick(x,a) -> tick(y,a);
```
Copy and paste this in the Semantics box. We will try to prove axioms A1 and BKS2.

In the Axiom box, type alt(x,y) = alt(y,x) and click on Prove it! This should return True, as one would except. Do note, however, that to prove this axiom, one needs reflexivity (x <= x) as well. By default this inequality is added as auxiliary inequality. You can turn this of by unchecking the add reflexivity box. (Try it and see what happens.)

Now lets take a more complex axiom. Enter seq(star(x,y),z) = star(x,seq(y,z)) in the Axiom box. This is axioms BKS2 ((x*y).z = x*(y.z)). When you click on Prove it! you will notice that it takes a while before a result is returned. This is often the case when equalities cannot be proven sound by the prover.

The output should be similar to the following:

```False
might need "@APPL@"("@R@"(),"seq"("seq"("p20","star"("p","q0")),"q"),"seq"("p20","star"("p","seq"("q0","q")))) (in context "trans"("p","a","p20"))
error: timeout
```
It states that could not find a prove within the given time limit. However, it also suggest that the reason for this is that it might need an auxiliary equality. Translated, it says that it thinks it needs the inequality seq(seq(p20,star(p,q0)),q) <= seq(p20,star(p,seq(q0,q))) (or x.(y*z).v <= x.(y*(z.v))). It also gives some context information. In this case we also have that p can do a transition to p20. We do not need this information in this case.

Now take the advice of the prover and add the equality seq(seq(p20,star(p,q0)),q) = seq(p20,star(p,seq(q0,q))) to the Auxiliary equalities box. Do not forget to append a semicolon (;) to it (see Syntax above). Clicking on Prove it! will now result in a positive answer.

## References

 Fok94 W. Fokkink, Clocks, Trees and Stars in Process Theory. PhD. thesis, University of Amsterdam, 1994. vW08 M. van Weerdenburg, Automating Soundness Proofs. SOS 2008, to appear.