It is shown that the following minimum cover problems are NP-hard, even for polygons without holes: (1) covering an arbitrary polygon with convex polygons; (2) covering the boundary of an arbitrary polygon with convex polygons; (3) covering an orthogonal polygon with rectangles; and (4) covering the boundary of an orthogonal polygon with rectangles. It is noted that these results hold even if the polygons are required to be in general position.>

The problem of covering a polygon with convex polygons has proven to be very difficult, even when restricted to the class of orthogonal polygons using orthogonally convex covers. We develop a method of analysis based on dent diagrams for orthogonal polygons, and are able to show that Keil's Ο(n2) algorithm for covering horizontally convex polygons is optimal, but can be improved to Ο(n) for counting the number of polygons required for a minimal cover. We also give an optimal Ο(n2) algorithm for covering another subclass of orthogonal polygons. Finally, we develop a method of signatures which can be used to obtain polynomial time algorithms for an even larger class of orthogonal polygons.

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results. In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus.

In this paper we introduce a formal model for random access computers and argue that the model is a good one to use in the theory of computational complexity. Results are proved which compare run times for recognizing sets using this model (which has a fixed program) with a stored program model and with Turing machines. The main result, theorem 3, shows the existence of a time complexity hierarchy which is finer than that of any standard abstract computer model. An Algol-like programming language is introduced which facilitates proofs of the theorems.