[
Lists Home |
Date Index |
Thread Index
]
Miles Sabin wrote:
> Paul Prescod wrote,
>
>>No, it isn't expressible in OWL 1.0. But it also doesn't require
>>Turing-completeness so OWL 2.0 will probably handle it. It is a
>>stated objective!
>
>
> Which implies giving up decidability.
I do not believe that is true.
"In this paper we propose using arithmetic equation solving instead of
tableau systems as the basic inference algorithm. It is, however, not
the purpose of this paper to investigate arithmetic equation solving
itself; we assume suit-able algorithms are available (they can actually
be downloaded from the internet). Therefore we do not specify a
particular arithmetic language. The language depends on the available
arithmetic equation solver. Most of them can solve systems of linear
equations and in-equations. In this case only addition, subtraction and
multiplication with numbers is allowed. More advanced systems also allow
for certain non-linear terms. The general non-linear Diophantine
equation problem, however, is undecidable (Hilbert's 10th problem
[13]). Therefore the arithmetic language should not be too expressive."
http://www.pms.informatik.uni-muenchen.de/mitarbeiter/ohlbach/homepage/publications/DL/mdla/mdla.pdf
Paul Prescod
|
