Handbook of Automated Reasoning

Chapter 6

Computing Small Clause Normal Forms

Andreas Nonnengart; Christoph Weidenbach

Contents

1  Introduction     337

2  Preliminaries     338

3  Standard CNF-Translation     340

3.1  Formula Simplification     341

3.2  Negation Normal Form     341

3.3  Miniscoping     343

3.4  Variable Renaming     344

3.5  Standard Skolemization     345

3.6  Clause Normal Form     346

3.7  Clause Simplification     347

4  Formula Renaming     347

5  Skolemization     352

6  Simplification     359

6.1  Equality     360

6.2  Atom Definitions     361

6.3  Binary Decision Diagrams     362

7  Bibliographic Notes     363

8  Implementation Notes     364

Bibliography     365

Index     367

1 Introduction