Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Gost ("**G**F **O**ne Minus **S**atisfiability **T**ester")
is a Lisp implementation of this algorithm. The implementation and some
empirical results are presented in [Hladik00]
(BibTeX).

*gost.lisp* contains the tableau algorithm for testing satisfiability
of a GF1- formula. *gost-simplify.lisp* contains auxiliary functions
for syntactic preprocessing of a formula. Both files are contained in gost.tar.gz.

To run the "LWB" benchmark, you need the files contained in the file gost-lwb.tar.gz. The benchmark formulae themselves are slightly modified in order to make parsing and translation easier.

To run the "TANCS-QBF" benchmark, you need the file gost-tancs.tar.gz.
Again, the syntax of the formulae is slightly modified.

If you want to test your own formulae, you need to compile and load
*gost.lisp*
and *gost-simplify.lisp*. After that, you can test a formula with
*(solve
<formula>)*. If there is a model, a (list of) models is returned,
otherwise NIL. The syntax of <formula> is described below. For formulae
including quantifiers, there are several restrictions to obey, in particular
the formulae have to be *guarded, *and there has to be a fixed *grouping
*of the variables appearing in the guard, as described in the papers
mentioned above.

Please make sure that you strictly follow the GF1- syntax, since Gost does not perform syntax checking, and using non-GF1- formulae may lead to strange results.

Formula | PL syntax | Gost syntax |

Variables | x_i | (? i) |

Predicates | P(x_i, x_j) | (P (? i) (? j)) |

Negation | NOT phi | (:NOT <phi>) |

Conjuncions | phi AND psi | (:AND <phi> <psi>) |

Disjunctions | phi OR psi | (:OR <phi> <psi>) |

Universal Quantification | FORALL (x_i, ... , x_n, )
(G(x_i, ... , x_n, y_j, ... , y_m) -> phi (x_i, ... , x_n)) |
(:ALL ((? i) ... (? n))
(G (? i) ... (? j_n) (? j) ... (? m)) <phi>) |

Existential Quantification | SOME (x_i, ... , x_n)
(G(x_i, ... , x_n, y_j, ... , y_m) AND phi (x_j, ... , x_n)) |
(:EX ((? i) ... (? n))
(G (? i) ... (? n) (? j) ... (? m)) <phi>) |

"True" | e.g. (phi OR (NOT phi)) | (:TOP) |

i, j, k etc are natural numbers.

phi and psi GF1- formulae, phi (x_i, ... x_n) is a formula with free
variables x_i, ..., x_n.

G(...) is the guard predicate.

RWTH Aachen, 52056 Aachen, Germany

All rights reserved.

The author makes no representations about the suitability of this software for any purpose. It is provided "AS IS" without express or implied warranty. In particular, it must be understood that this software is an experimental version, and is not suitable for use in any safety-critical application, and the author denies a license for such use.

You may use, copy, modify and distribute this software for any noncommercial and non-safety-critical purpose. Use of this software in a commercial product is not included under this license. You must maintain this copyright statement in all copies of this software that you modify or distribute.