Saga
Saga is Lisp program implementing a tableau algorithm for the Guarded Fragment of Predicate Logic described in C. Hirsch and S. Tobies: A Tableau Algorithm for the Clique Guarded Fragment. The name stands for "Satisfiability Algorithm for the Guarded Fragment". A detailed description can be found in J. Hladik: Implementierung eines Entscheidungsverfahrens für das Bewachte Fragment der Prädikatenlogik (in German).
Files
The system consists of several files:
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.
Usage
If you want to run one of the benchmarks, download the appropriate tarfile, unpack it and load the corresponding benchmark file, saga-bench-lwb.lisp, saga-bench-tancs.lisp or saga-bench-gf.lisp. Call (recomp) to compile the source files, then (bench) (tbench) or (gfbench) to run the benchmark. For LWB, the results are printed, for TANCS and GF, they are written to the *outfile* specified in saga-bench-tancs/gf.lisp.
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.
Syntax
| 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.
Copyright
Copyright (C) 2001 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.