This paper shows that the nice properties of logic programs extend to definite clause specifications over arbitrary constraint languages. The notion of a constraint language sees a constraint as a piece of syntax with unknown internal structure that constrains the values variables can take in interpretations. Examples of constraint languages are Predicate Logic and its sublanguages as well as attributive concept description languages developed for knowledge representation. Our framework generalizes the constraint logic programming scheme of Jaffar and Lassez to make it applicable to knowledge representation: the constraint language is not required to be a sublanguage of predicate logic and may come with more than one interpretation, and the interpretations of the constraint language are not required to be solution compact. We present a semantic type discipline for our generalized definite clause specifications and establish a notion of well-typedness that is decidable provided the underlying constraint language is decidable. Finally, we give a type inference rule for computing most general well-typed weakenings of specifications.
Download PDF Show BibTeX
Login to edit