PizEAndSATO is a system for CNF first order problems with a finite
Herbrand universe.
It is implemented by combining the ground-instance generating
program PizE with the propositional prover
SATO.
PizE is based on the
E libraries.
PizE and SATO are combined with a shell script called And.
PizEAndSATO has been created by
Geoff Sutcliffe -
Had the idea, wrote a perl version of PizE (called Pize),
collected a copy of SATO, wrote the And script, realised that Pize
was too slow, and spoke to ...
Stephan Schulz - Wrote the super PizE, refused to stop improving
it, is now thinking about writing a propositional decision procedure like
SATO, which was written by ...
Hantao Zhang -
Designed and implemented SATO (not specifically for PizEAndSATO).
In gastronomic terms, we sometimes think of PizEAndSATO like this ...
And
... but more often we think of it like this ...
... because we would be please to see it scare this ...
