🚀 go-pugleaf

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