Handbook of Automated Reasoning

Chapter 5

Normal Form Transformations

Matthias Baaz; Uwe Egly; Alexander Leitsch

Jean Goubault-Larrecq; David Plaisted Second readers

Contents

1  Introduction    275

2  Notation and Definitions    278

3  On the Concept of Normal Form    287

4  Equivalence-Preserving Normal Forms    289

5  Skolem Normal Form    295

6  Conjunctive Normal Form    306

6.1  Nonstructural versus Structural Transformations to CNFs    312

6.2  Comparing Different Structural Transformations    317

6.3  Experimental Results    322

7  Normal Forms in Nonclassical Logics    323

7.1  Intuitionistic Logic    323

7.2  Some Other Nonclassical Logics    327

8  Conclusion    328

Bibliography    328

Index    332

1 Introduction

Normal forms traditionally ...