Model Finiteness and Funetionality in a Declarative Language with Oid Invention

Two important properties of IsaLog programs are studied: model niteness and functionality. Finiteness refers to the property of a program of having a nite model over every input instance. Functionality requires a model to contain no contradictory information about object values. These two properties are shown to be undecidable. This is a consequence of the ability of IsaLog programs to simulate computations of arbitrary Turing machines, provided their input is coded as a suitable instance. Weakly recursive programs, a restricted class of IsaLog programs, is then investigated. It is shown that every weakly recursive program admits a nite model over every input instance. Moreover, models for this class of programs can be computed in polynomial time with respect to the number of objects in the input instance.