A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae

Stephan Schulz

A near-propositional CNF formula is a first-order formula (in clause normal form) with a finite Herbrand universe. For this class of problems, the validity problem can be decided by a combination of grounding and propositional reasoning. However, naive approaches to grounding can generate extremely large ground formulae. We investigate various means to reduce the number of ground instances generated and show that we can increase the number of problems that can be handled with reasonable resources.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.