On Tue, Aug 07, 2007 at 02:55:23PM -0500, Chris Menzel wrote:
> ...It is (among other things) completeness that makes FOL so important
> to automated reasoning, as it means that, whenever A is a logical
> consequence of S in a first-order logic, there is actually a *proof*
> of A from some (finite) subset of S. (Alas, finding that proof is
> another kettle of fish entirely, which is why we have more
> constrained, less expressive logics like description logics and their
> ilk.) (01)
An alert ontolog-forum reader has pointed out to me that "ilk" can have
pejorative connotations and hence is often restricted to contexts where
the persons or things referenced are in some way unsavory or
undesirable, e.g., "fascists, racists, and others of that ilk." (That
example actually comes from OS X's built in dictionary program.) For
the record, I want to point out that I had no such usage in mind above.
My point was purely logical: that, due to the general undecidability of
full FOL, research in automated reasoning has led to the development of
more contrained logics that trade some measure of expressive power for
decidability. DLs of course constitute a particularly salient and
important example, as they underlie OWL and form the basis of a variety
of ontology-oriented automated reasoning systems like Racer. The
superfluous and potentially misleading tag "and their ilk" above should
simply have been left off. (02)
-chris (03)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (04)
|