[
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 ...
Cheers,
Miles
|
