This system has been developed as a part of the research project DisLoP funded by DFG.

The form below can be used to generate sets of ground clauses which provide interesting test cases for propositional theorem provers. The idea is the following: a graph and an NP-complete problem are selected and then from the graph a set of clauses is generated so that the clause set has a model iff there is a solution for the given problem for this particular graph.

You can choose between two different representations of the clause set:

- a syntax that uses ISO Prolog as far as possible but where
disjunctions are represented using a predicate
disj/2, and negations are
represented using not/1, e.g.
`a disj b disj c :- not d , e.`

a disj b disj d.

bottom :- a,b,c.Empty clause heads are represented by

`bottom`. - the syntax of the mm minimal model reasoner
that uses "<-" instead of ":-" and
represents disjunctions by semicolons, e.g.
Empty clause heads are represented by`a ; b ; c <- d , e.``false`. Empty clause bodies are represented by`true`.

Note: The graphs are generated using TheoryBase, a program developed at the University of Kentucky, which creates graphs of different types on the basis of the Stanford GraphBase by D. Knuth.

visitors since June 27, 1997.

Maintained by: K. Erk <katrin@informatik.uni-koblenz.de> and C. Aravindan <arvind@informatik.uni-koblenz.de>

$Author: arvind $ $Date: 1997/10/17 14:20:27 $