simplify - Program Simplification of Non-Ground Programs
The toolbox simplify provides a first a prototype for program
simplification of non-ground
disjunctive datalog programs with negation under the
stable model semantic.
The toolbox scans programs with respect to two potential replacements,
G-SUBS, G-LSH and indicates which rules are applicable to
those simplifications. Hereby,
Both replacement techniques are described in [E+06]. For a description of the implementations see Chapter 5.1 of [Traxler06], or [ETW06].
- G-SUBS (rule subsumption) seeks for rules which can be eliminated from the input program, such that strong equivalence is preserved.
- G-LSH (local shifting) seeks for proper disjunctive rules which can be shifted into
normal rules, such that uniform equivalence is preserved.
Download simpl-1.0.tar.gz and unpack it. You might need to change the variable
$DLV in the perl scripts
simplify_glsh.pl. This variable contains the location of your DLV system. Otherwise, make sure that the
PATH variable of your command shell contains the location of your DLV system.
At the moment our toolbox consists of two scripts which take as input
a program P in DLV syntax.
Both scripts are called by the
As an example take the file
After calling it with
on the command line it first outputs rules which apply for
subsumption and then rules which apply for shifting:
Scanning for Rule Subsumption...
b(X) v b(a) :- edge (X,Y), node(X), node(a), not r(X), not g(a), not g(X).
[subsumbed by r(Y) v b(Y) v g(Y) :- node(Y).]
Scanning for Local Shifting...
r(Y) v b(Y) v g(Y) :- node(Y).
For the exact definitions of G-SUBS and G-LSH please see [E+06] or [T06].
The benchmarks reported in [ETW06] are the following
graphs.tar.gz contains 70 programs which encode
3-colorability as rule-subsumption problems.
sat.tar.gz contains 200 programs which encode
satisfiabiliy as rule-subsumption problems.
exp.tar.gz contains 12 proper disjunctive programs
which are tested for local shifting.
Last update: 2006-04-27 by Stefan Woltran