[DL] Horn clauses and DLs

[Enrico Franconi]

On 9 Oct 2004, at 19:38, Rodrigo de Salvo Braz wrote:
> On Tue, 5 Oct 2004, Enrico Franconi wrote:
>> 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?

I really mean structured syntax - where this argument is not as trivial 
as it seems.
On the one hand, there are all the long standing arguments from 
cognitive science showing that "frames/features" are a basic 
representation mean for humans; this started all the KL-One and 
derivative stuff (up to DLs). So DLs can be used in a intuitive way by 
humans for KR.
On the other hand, there is the more recent argument from logicians 
such as van Benthem, Gabbay, Vardi et al, about the "guarded fragment" 
(GF) of FOL being the "right" fragment of FOL - DLs are just a special 
interesting case of the GF. See, e.g., "The Guarded Fragment: Ins and 
Outs" by Carlos Areces, Christof Monz, Hans de Nivelle, Maarten de 
Rijke, at <http://citeseer.ist.psu.edu/431035.html>, for a very nice 
comparative intro to the GF. The GF enjoys nice semantical properties 
from the modal logic point of view (they can be seen as the most 
general framework in which most modal logics fit in), but most 
importantly from our point of view it enjoys what Vardi called the 
"robust decidability" property: not only is the basic ALC DL decidable, 
but it remains decidable when we add temporal constructs, fixed point 
operators, counting, nominals, etc.

cheers
--e.