GrAnDe
GrAnDe (Ground And Decide)
is a system for CNF first order problems with a finite Herbrand universe.
It is implemented by combining the ground-instance generating
program eground with the propositional prover
ZChaff.
eground is based on the
E libraries.
eground and ZChaff are combined with a Perl
script called And.
GrAnDe has been created by:
- Geoff Sutcliffe -
Had the idea, wrote a grounding program in perl (called
Pize), wrote And, realised that Pize is
too slow, and asked Stephan for help.
- Stephan Schulz -
Wrote eground and refused to stop improving it.
- Sharad Malik and
his people,
who wrote ZChaff for their own reasons, and have kindly
allowed us to use it in GrAnDe.
The latest version of GrAnDe can be created, by following these
instructions (we cannot provide a single source tarball, due to licensing
restrictions):
- Get and build
E, 0.63 or later.
(Here's a local copy of the E tarball.)
- Get and build
ZChaff.
(Here are local copies of the ZChaff
Linux binary and
Solaris binary.
You have to
ask the ZChaff people directly if you need the source.)
- Get And.
- Place eground (from the PROVER subdirectory of
E), the ZChaff executable, and And in a
directory.
- Make adjustments for your local environment
- Set the perl directory in And.
- Set the $EGround and $Decide variables in
And.
- Sit back, and say "Wow, that's GrAnDe!"