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

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

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.