[DL] Horn clauses and DLs

[Rodrigo de Salvo Braz]

On Tue, 5 Oct 2004, Enrico Franconi wrote:

> Horn clauses encode only polynomial problems. Standard DL's (from ALC
> up, including the DL's implementted in systems such as iFaCT and Racer)
> encode up to EXPTIME problems (and coNP in data complexity).

Good point. What about clauses in general? I realize that is equivalent to
full FOL but does that mean it is completely ruled out from practical
applications? Or maybe some extension of Horn, like functionless clauses?

> > The reason I am asking this is because I get the feeling from many
> > people
> > that if you have some practical application in which you want a
> > tractable
> > language, then you should immediately restrict yourself to choosing
> > from
> > DL languages.
>
> Where do you get this feeling from?

I got that from a couple of professors I talked to, although they are not
DL people. Also the literature in DL gives me that impression; it seems to
imply that once you start concerning yourself with tradeoffs between
expressivity and tractability, then you step into the DL area. Of course
that may have been my erroneous interpretation.

> There is a wide variety of decidable (and poly) fragments of FOL - not
> only Horn clauses. One reason for not considering them in KR is that
> they do not offer a "structured" way to represent knowledge, which I
> believe is a crucial feature of KR languages. Other than that, I am in
> favour of any well-founded logic-based formalism :-)

What do you mean by "structured"? Structured as in a structured syntax, or
structure as in taking advantage of structure in domain, like temporal
reasoning?

Thanks,

Rodrigo