OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.


Help: OASIS Mailing Lists Help | MarkMail Help



   Re: [xml-dev] Decidability

[ Lists Home | Date Index | Thread Index ]

Paul Prescod wrote,
> "As soon as arithmetics comes into play, tableau approaches
> become very diffcult to use. For example in a concept definition
> parents-of-many-boys = parent ^ has-son >=2 * has-daughter
> (parents-of-many-boys are parents having more than twice as many sons
> than daughters) the consistency problem amounts to checking whether x
> * 2y has a non-negative integer valued solution."
> How is this not an arithmetic constraint? Of course the technique
> isn't "general", as in covering all arithmetic. But it is
> nevertheless designed to allow arithmetic constraints.

It is an arithmetic constraint: of a very restricted form.

> My claim is that there is a _SUBSET_ of arithmetic which is
> decidable.

Of _course_ there are subsets of arithmetic which are decidable. And 
there are subsets of XSLT and Java which are decidable too.

In all cases the questions are: Is the subset large enough to be useful 
in practice? And is the decidability game worth the candle anyway?

The first question relates to expressive power: make the restrictions 
too severe and it can be impossible or very difficult to say the things 
you want to say.

The second points to the fact that the 'finite' in 'finite decision 
procedure' can be very, very, very big indeed. Who cares if a decision 
procedure will terminate in finite time if we'll all be long dead 
before it's done? Practically speaking, the system might as well be 
undecidable: decidability != feasibility.

> If you want to continue the discussion I suggest we take it to
> www-rdf-interest where logic experts will be able to weigh in (unless
> you claim to be an expert).

Be my guest ...




News | XML in Industry | Calendar | XML Registry
Marketplace | Resources | MyXML.org | Sponsors | Privacy Statement

Copyright 2001 XML.org. This site is hosted by OASIS