# 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 ("**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).

## 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.