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.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
- Schulz, Stephan; Sutcliffe, Geoff: System description: GrAnDe 1.0 (2002)