Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

**syntax:** `(ws1s &optional (fnums *) (examples? t)
(automaton? nil) (traces? nil) (verbose? t) (defs !) theories rewrites
exclude)`

**effect: **This strategy implements a decision procedure for the Weak
Second-order monadic logic of 1 Successor (WS1S). The supported fragment
of WS1S includes boolean expression, arithmetic on the natural numbers
restricted to addition/subraction with/from a constant, and operations on
finite sets over the naturals like union, intersection, set difference,
addition and removal of a natural. Predicates include arithmetic
comparisons like `<`, `<=`, `>`,
`>=`, equality, disequality, the subset relation, and membership
in the form `P(i)`. There is quantification over the booleans, the
natural numbers, finite sets of naturals, and predicate subtypes of the
aforementioned types built from formulas in the set just
described. Furthermore, natural numbers, and finite sets of natural
numbers may also be described using the `the` operator;
e.g. ripple-carry addition may be defined as:

+(P, Q: finite_set[nat]): finite_set[nat] = the({R: finite_set[nat] | EXISTS (C: finite_set[nat]): NOT(C(0)) AND FORALL (t: nat): (C(t + 1) = ((P(t) AND Q(t)) OR (P(t) AND C(t)) OR (Q(t) AND C(t)))) AND (R(t) = P(t) = Q(t) = C(t))});

Using this definition, lemmas such as

plus_assoc: LEMMA FORALL (X, Y, Z: finite_set[nat]): X + (Y + Z) = (X + Y) + Z

are proven to be valid by simply calling `(WS1S)`.

In a first step, the WS1S strategy rewrites the formulas specifed by
`FNUMS`. The resulting formulas are then translated, using the
rule `WS1S-SIMP`, to an automaton which recognizes the language of
their interpretations. Hereby, subformulas that do not appear to be in
the WS1S fragment are abstracted away by introducing new parameters. If
the final automaton recognizes the full set, the `FNUMS` formulas
are replaced by `TRUE`; otherwise, these formulas are left
unchanged.

The `DEFS`, `THEORIES`, `REWRITES`, and
`EXCLUDE` arguments are used to install rewrites. For a precise
description of their meaning see e.g. `AUTO-REWRITE-THEORY` or
`INSTALL-REWRITES`.

In case where the formulae specified by `FNUMS` are neither
valid nor unsatisfiable both a witness and a counterexample are displayed
if the flag `EXAMPLES?` is set. Hereby, expressions are displayed
for both the free variables in the `FNUMS` formulas and the newly
introduced abstraction parameters. An alternative, trace-oriented view of
the examples are displayed if the `TRACES?` flag is on.

With the `AUTOMATON?` flag turned on, the constructed automaton is
displayed.

Translation messages are being displayed whenever the flag
`VERBOSE?` is set to `T`. Messages like "Abstracting..."
indicate the introduction of a new parameter, and "Not abstractable ..."
indicates that there is a free occurrences of a bound variables in the
current subformula. In this case, the translation process aborts. A
second source of failure in the translation process comes from quantifiers
which contain bindings not included in WS1S. In these cases, a message
like "Not in ws1s: ... in ..." is displayed and the translation process
aborts.

These messages may be helpful in detecting expressions that are not
known to be in WS1S by the translator. In these cases, it might be useful
to decorate these expressions with appropriate type coercions
(e.g. `{x: nat | x = 1 OR x = 2} :: finite_set[nat]`) to support
the translation process.

**usage:** `(ws1s 1 :examples? nil :verbose?? nil)` Tries to
reduce formula 1 to true; suppresses both translation messages and the
display of a witness and a counterexample in case this formula is neither
valid nor satisfiable.

**errors:** "Formula ... not in WS1S"

The translation process could not construct a DFA for
the formula ...

**notes:** The WS1S strategy uses the libraries of Mona to
construct DFAs. Mona was developed at BRICS - see http://www.brics.dk/~mona for
details.

Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

*
Last modified: Fri 18 May 2007 01:24 UTC
Maintainer: Sam Owre
*