Automated reasoning with quantified formulae
David Greve · 2009
ACL2 allows users to define predicates whose logical behavior mimics that of universally or existentially quantified formulae. Proof support for such quantification, however, is quite limited. We present an ACL2 framework that employs tables, computed hints and clause processing to identify quantified formulae and to skolemize or instantiate them when possible. We demonstrate how the framework can be used to prove automatically the forall-p-append example presented in the ACL2 documentation.