A BDD-Based Simplification and Skolemization Procedure

Publisher Website
Google Scholar
Abstract
We introduce a new technique to simplify and skolemize first-order formulas, based on binary decision diagrams, or BDDs. This technique is more computation-intensive than previously known ones, but in general provides better skolemized forms that attempt to reduce the number of false dependencies. This technique can also be seen as a practical way of simplifying first-order formulas before feeding them to an automated theorem prover.

This publication has 0 references indexed in Scilit: