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

Gost

GF1- is a description logic which is defined as a restriction of the "First Guarded Fragment". The language itself, its complexity (PSPACE) and a satisfiability algorithm are described in [LutzSattlerTobies99] (BibTeX).

Gost ("GF One Minus Satisfiability Tester") is a Lisp implementation of this algorithm. The implementation and some empirical results are presented in [Hladik00] (BibTeX).

Files

The system consists of several files:

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.

Usage

If you want to run one of the benchmarks, download the appropriate tarfile, unpack it and load the corresponding benchmark file, gost-bench-lwb.lisp or gost-bench-tancs.lisp. Call (recomp) to compile the source files, then (bench) or (tbench) to run the benchmark. For LWB, the results are printed, for TANCS, they are written to the *outfile* specified in gost-bench-tancs.lisp.

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.

Syntax

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.

Copyright

Copyright (C) 2000 by Lehr- und Forschunggebiet Theoretische Informatik
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.