Gost ("GF One Minus Satisfiability Tester") 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|
|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.