# Exponentialblowup from conjunctiveto 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

# Solution 1

 (1)

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

# Solution 2

 (2)

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

# 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.

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

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