[XML-DEV Mailing List Archive Home] [By Thread] [By Date] [Recent Entries] [Reply To This Message] Re: Semantic Web and First Order Logic
Thomas B. Passin wrote, > [Miles Sabin] > > This is easy to express in second-order logic, or in first-order > > logic plus set theory (the "plus set theory" bit means that you can > > forget about decidability). Not so easy in plain first-order logic. > > Hmm, it depends on your definition of FOL, I suppose, and it also > depends on how you model things. I assumed that FOL includes types > and your "plus set" stuff Those'd be first-order theories (ie. they're expressed in first-order logic) but they're not first-order logic. And they're not necessarily decidable (a type theory might be, set theory isn't). > (but a set of individuals is a kind of quantifier over individuals, is > it not?). In first-order set-theory a set of individuals is an individual in it's own right, not a quantifier. > I take it that in FOL, quantifiers range over individuals while in > second order logic, quantifiers can range over predicates and > relations. Is that what you understand? More or less. > Applying this to your example, if you used Red(widget), then your > statement would be about the predicate (ie., Red), and therefore > second order, right? Yup. > But the redness can be modeled in other ways. Oh, sure. I mentioned one: first-order logic plus set-theory. > For example, we could say Color(x,red) and IsPrimaryColor(red). Then > your example could be stated something like this - > > {for all x,y| Widget(x) and Color(x,y) and IsPrimaryColor(y)}==> > Surcharge(x,5%) > {Widget(x) and Color(x,red)} > {IsPrimaryColor(red)} > > Now we are only making statements about the arguments, and they are > individuals, not predicates or relations. So it is FOL, right? And > an SQL query could extract the surcharge from a database. It's a first-order _theory_, but it's not first-order _logic_. Chances are that the first-order theory of widget-colour-surchages will be decidable, but that's not true of first-order theories in general: viz. arithmetic, set-theory ... And this is where the constraint that Len was complaining about bites: the base-level logical frameworks being considered for the SW insist on decidability, and that excludes many practically useful, tho' formally undecidable first-order theories. Here's something else you might try to first-orderize nicely, Some widgets attach only to one another You can express this is second-order logic, {exists P | {exists x | Px } and {for all x | Px ==> Widget(x) and {for all y | attach(x, y) ==> Py } } } and you can express it in first-order set theory, {exists X | {exists x | member(x, X) } and {for all x | member(x, X) ==> Widget(x) and {for all y | attach(x, y) ==> member(y, X) } } } but neither second-order logic nor first-order set theory are decidable, so neither of these renderings is compatible with the frameworks touted for the SW which respect the decidability constraint. Can you come up with a rendering which is? OTOH, can you persuade me that this kind of assertion is irrelevant to business applications? All it's doing is saying that there's a binary relation ("attach" in the example) which partitions the domain of widgets in a particular way. That seems like a useful kind of thing to be able to say. Cheers, Miles
|
PURCHASE STYLUS STUDIO ONLINE TODAY!Purchasing Stylus Studio from our online shop is Easy, Secure and Value Priced! Download The World's Best XML IDE!Accelerate XML development with our award-winning XML IDE - Download a free trial today! Subscribe in XML format
|