Xref: utzoo comp.lang.prolog:991 comp.ai:1790 Path: utzoo!attcan!uunet!husc6!bloom-beacon!bu-cs!purdue!decwrl!labrea!agate!eos!ames!pacbell!att!alberta!ubc-cs!bay.cs.ubc.ca!mack From: mack@bay.cs.ubc.ca (Alan Mackworth) Newsgroups: comp.lang.prolog,comp.ai Subject: Re: Logic Programming and Vision Keywords: vision research, prolog, logic programming Message-ID: <2780@ubc-cs.UUCP> Date: 20 May 88 17:09:03 GMT References: <632@hub.ucsb.edu> <2868@cvl.umd.edu> Sender: nobody@ubc-cs.UUCP Reply-To: mack@bay.cs.ubc.ca (Alan Mackworth) Organization: UBC Department of Computer Science, Vancouver, B.C., Canada Lines: 40 I responded privately on this query but since it has come up it's worth following up. Ray and I have produced a logical framework for depiction and image interpretation described in: R. Reiter & A.K. Mackworth, "The Logic of Depiction" RBCV-TR-87-18 Dept. of Computer Science, Univ. of Toronto, Toronto, ON, Canada, also TR-87-24, UBC Dept. of Computer Science, Vancouver, B.C., Canada, 1987. Abstract We propose a theory of depiction and interpretation that formalizes image domain knowledge, scene domain knowledge and the depiction mapping between the image and scene domains. This theory is illustrated by specifying some general knowledge about maps, geographic objects and their depiction relationships in first order logic with equality. An interpretation of an image is defined to be a logi- cal model of the general knowledge and a description of that image. For the simple map world we show how the task level specification may be refined to a provably correct implemen- tation by invoking model preserving transformations on the logical representation. In addition, we sketch logical treatments for querying an image, incorporating contingent scene knowledge into the interpretation process, occlusion, ambiguous image descriptions, and composition. This approach provides a formal framework for analyzing existing systems such as Mapsee, and for understanding the use of constraint satisfaction techniques. It also can be used to design and implement vision and graphics systems that are correct with respect to the task and algorithm lev- els. We transform the specification from FOL+equality to propositional form so our model theoretic approach has simply an NP-hard problem (SAT) to deal with. The transformation can be seen as producing a Constraint Satisfaction Problem. The known algorithms for CSP's can be seen as approximation algorithms for SAT, in this case. The natural implementation language for our framework is Prolog. Alan Mackworth