saga.lisp contains the tableau algorithm for testing satisfiability of a GF formula. saga-simplify.lisp contains auxiliary functions for syntactic preprocessing of a formula. Both files are contained in saga.tar.gz.
To run the "LWB" benchmark, you need the files contained in the file saga-bench-lwb.tar.gz. The benchmark formulae themselves are slightly modified in order to make parsing and translation easier.
To run the "TANCS-QBF" and "TANCS-PSAT" benchmarks, you need the file saga-bench-tancs.tar.gz. Again, the syntax of the formulae is slightly modified.
There exists a set of random generated GF-Formulae that can also be used for benchmarking. The corresponding files and the formula generator are contained in saga-bench-gf.tar.gz.
If you want to test your own formulae, you need to compile and load saga.lisp and saga-simplify.lisp. After that, you can test a formula with (construct-tableau <formula>). If a model is found, it is returned, otherwise NIL. The syntax of <formula> is described below.
Please make sure that you strictly follow the GF syntax, since Saga does not perform syntax checking, and using non-GF formulae may lead to strange results.
| Formula | PL syntax | Saga syntax |
| Variables | x_i | (? i) |
| Predicates | P(x_i, x_j) | (P (? i) (? j)) |
| Equality | x_i = x_j | (:EQ (? 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,y_j, …, y_m)) |
(: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 y_j, … , y_m)) |
(: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 GF formulae, phi (x_i, ... x_n) is a formula with free
variables x_i, ..., x_n.
G(...) is the guard predicate.