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

 


Help: OASIS Mailing Lists Help | MarkMail Help

 


 

   Decidability

[ Lists Home | Date Index | Thread Index ]

Miles Sabin wrote:
> Paul Prescod wrote,
> 
>>Miles Sabin wrote:
>>
>>>Which implies giving up decidability.
>>
>>I do not believe that is true.
> 
> 
> Believe what you like ... arithmetic is undecidable, so extending a DL 
> with arithmetic gets you an undecidable system.

I don't claim to be a logician, but I do have basic reading skills.

> Did you even read that paper? Or did you just grep it for something 
> which superficially sounded like it supported your argument? 

I skimmed it, which is different than grepping it.

 > ... The
 > authors aren't talking about expressing general arithmetic contraints
 > in DLs, they're talking about using an arithmetic equation solver to
 > _implement_ standard DL inference (as opposed to using a tableau
 > system). That's what it says in the very first sentence you quoted!

The reason they propose to use an arithmetic equation solver is to be 
able to solve arithmetic equations in description logics constraints:

"The class of description logics suitable for the proposed methods is 
strong on the arithmetical side. In particular there may be complex 
arithmetical conditions on sets of accessible worlds (role fillers)."

...

"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.

My claim is that there is a _SUBSET_ of arithmetic which is decidable. 
For instance:

http://thoralf2.uwaterloo.ca/htdocs/linear.html
http://www.alpertron.com.ar/QUAD.HTM

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).

  Paul Prescod





 

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

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