Exponential blowup from conjunctive
to disjunctive normal form

Wolfgang Slany
http://slany.org/wolfgang/
http://www.dbai.tuwien.ac.at/proj/pf2html/

April 23, 2002

Abstract:

HTML version of a sample proof that uses Lamport's proof style [1], illustrating how structured proofs can be converted to HTML pages via LATEX2HTML enriched with extensions for Lamport's proof style. Note that we try on purpose to carry out Lamport's rule of thumb to ``expand the proof until the lowest level statements are obvious, and then continue for one more level'' in order to illustrate the principles of structured hyper-proofs.

Problem (cf. [2]):

What is the disjunctive normal form of

\begin{displaymath}(\mbox{\htmladdnormallink{$x_1$}{http://foldoc.doc.ic.ac.uk/f...
...oc.cgi?and}} (x_2 \vee y_2) \wedge \dots \wedge (x_n \vee y_n)?\end{displaymath}

Solution 1


$\displaystyle \left. \begin{array}{rcc}
(x_1 \vee y_1) \wedge (x_2 \vee y_2) \w...
...addnormallink{$2^n$}{http://foldoc.doc.ic.ac.uk/foldoc/foldoc.cgi?Exponential}}$ $\textstyle ~$ $\displaystyle ~$ (1)

The resulting disjunctive normal form is exponentially blown up compared to the size of the original conjunctive normal form.

show proof





Solution 2


$\displaystyle \left. \begin{array}{rcc}
(x_1 \vee y_1) \wedge (x_2 \vee y_2) \w...
...addnormallink{$2^n$}{http://foldoc.doc.ic.ac.uk/foldoc/foldoc.cgi?Exponential}}$ $\textstyle ~$ $\displaystyle ~$ (2)

The resulting disjunctive normal form is exponentially blown up compared to the size of the original conjunctive normal form.

show proof







Acknowledgements

The help and comments of Marcus Carotta, Wolfgang Goedl, Martina Osztovits, and Helmut Veith are gratefully acknowledged.

Bibliography

1
Leslie Lamport, 1993, How to write a proof. In Global Analysis of Modern Mathematics, pp. 311-321. Publish or Perish, Houston, Texas, February 1993. A symposium in honor of Richard Palais' sixtieth birthday (also published as SRC Research Report 94). http://research.microsoft.com/users/lamport/proofs/src94.ps.Z

2
Christos H. Papadimitriou, 1994, Problem 4.4.5. In Computational Complexity, p. 84. Addison-Wesley.

About this document ...

Exponential blowup from conjunctive
to disjunctive normal form

This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.56)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html 445

The translation was initiated by Glowacki Martin / TU Wien Studenten Account Kopie on 2002-10-01


URL of this proof as currently expanded for referencing and bookmarking purposes.

This HTML file was generated using the pf2html extension, version 0.03.
LaTeX2HTML + pf.sty (hypertext proofs).

Project homepage at http://www.dbai.tuwien.ac.at/proj/pf2html


Glowacki Martin / TU Wien Studenten Account Kopie 2002-10-01