[HN Gopher] Owl: A Logics Perspective
___________________________________________________________________
Owl: A Logics Perspective
Author : PaulHoule
Score : 41 points
Date : 2022-11-25 09:10 UTC (2 days ago)
(HTM) web link (owl.cs.manchester.ac.uk)
(TXT) w3m dump (owl.cs.manchester.ac.uk)
| zozbot234 wrote:
| Note that SHACL is in somewhat more common use these days, and
| can also be given a logical basis not unlike OWL:
| https://news.ycombinator.com/item?id=31890041 Given that both are
| part of Semantic Web standards, it's a bit surprising that this
| was not noticed before.
| PaulHoule wrote:
| OWL's got the tough problem that it is hard to know what it can
| do and what it can't do. What documentation there is
|
| https://www.w3.org/TR/2012/REC-owl2-direct-semantics-2012121...
|
| tells you how to convert an OWL ontology into a set of first-
| order logic axioms and presumably an OWL reasoner can do
| whatever a FOL reasoner could do on those axioms.
|
| Compared to other schema and ontology languages, OWL makes it
| possible to write an ontology in terms of logical definitions.
| For instance an "OddLotTrade" could be a "Trade" where the
| quantity is less than 100.
|
| The trouble is that OWL can't do math in the sense of "compute
| the body mass index from a person's height and weight and
| determine that the person is underweight if the BMI is under a
| threshold." If you have the BMI precomputed it can do that, but
| you can't define the BMI itself in OWL.
|
| There is a good reason for that which is that FOL + arithmetic
| is undecidable for reasons Kurt Godel discovered.
|
| You can write "logical definitions" in another sense with
| production rules, for instance you can match the height and
| weight and add a fact with the BMI, but you lose the ability
| the OWL reasoner has to validate the ontology as a whole (e.g.
| if you have an xn+yn=zn kindof rule you wish it would know that
| it could never be satisfied but that's a very hard proof.)
|
| That said, the ability to export OWL to FOL means you can use
| OWL tools to develop and validate an ontology and then add some
| beyond-OWL stuff to it to do some reasoning.
| wizeman wrote:
| > FOL + arithmetic is undecidable for reasons Kurt Godel
| discovered.
|
| Adding finite arithmetic (i.e. on N-bit words rather than
| mathematical integers) to FOL should not change the
| decidability of FOL, or does it?
| a1369209993 wrote:
| > Adding finite arithmetic [...] should not change the
| decidability
|
| No (unless you can implement arbitrary-precision arithmetic
| indirectly, which you frequently can), but then you have
| insane, nonsensical conclusions[0] due to integer overflow.
|
| 0: Eg, the mass of the earth (in grams) is less than the
| mass of the moon (in grams) if you use 64-bit ints - but
| that's _not_ true of their masses in kilograms or pounds.
| wizeman wrote:
| > No
|
| To be clear, you're saying that it _wouldn 't_ change the
| decidability, correct?
|
| > 0: Eg, the mass of the earth (in grams) is less than
| the mass of the moon (in grams) if you use 64-bit ints -
| but that's not true of their masses in kilograms or
| pounds.
|
| Which is why you should have used 256-bit ints for
| computing that answer ;)
| [deleted]
___________________________________________________________________
(page generated 2022-11-28 05:01 UTC)