[HN Gopher] Owl: A Logics Perspective
       ___________________________________________________________________
        
       Owl: A Logics Perspective
        
       Author : PaulHoule
       Score  : 33 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?
        
       | [deleted]
        
       ___________________________________________________________________
       (page generated 2022-11-27 23:01 UTC)