It has become evident in computational vision that there is a need to formalize the intuitions of existing vision systems. Any such formalization must allow the designer to explicitly reason about the capabilities and limitations of different representations and techniques. This thesis presents a logical axiomatization of shape-based object recognition in 2D scenes with occlusion and errors in edge detection, in a domain known as CardWorld. In particular, we introduce a family of eight theories which axiomatize the image and scene domain, polygonal shapes, depiction of shapes, reasoning about surface interiors, the depiction of surfaces as planar regions, the obscuring of surfaces in a scene, and the relationship between occlusion and depiction. We then introduce shape and depiction assumptions which allow us to restrict our attention to finite models of the CardWorld theories, and consequently specify prepositional theories which are logically equivalent to the CardWorld theories. In the final part of the thesis, we consider the com putational complexity of finding models of these prepositional theories. We show that in general, these tasks are NP-hard, but by exam ining restricted classes of images, we can identify tractable subclasses of the problems.