D-entailment games... [Was: Re: is rdf a regular logic? RIF? was: Coherent Logic (a.k.a Geometric Logic) and RDF?]

[I changed the topic, as this is irrelevant to the original thread.]


Very good, Aidan, I don't see any error in the reasoning.

Note that you do not need to appeal to RDFS recognising xsd:string. If 
we assume "proto-RDFS entailment", which I define exactly as RDFS 
entailment except that it does not impose that xsd:string and 
rdf:langString are recognised, then how can the inconsistency be proved?


--AZ



Le 22/01/2020 à 08:45, Aidan Hogan a écrit :
> off topic ...
> 
> On 2020-01-21 5:48, Antoine Zimmermann wrote:
> [snip]
>> D-entailment can be horribly complicated. Consider this example:
>>
>> rdf:Property rdfs:subClassOf xsd:boolean .
>>
>> Is this RDFS-recognising {xsd:boolean}-consistent?
> 
> 
> No. (If I'm not mistaken.)
> 
> First D-entailment (which must recognise xsd:string) will give us:
> 
>    xsd:string rdf:type rdfs:Datatype .        #1 [rdfs1]
>    "a" rdf:type xsd:string .                  #2 [semantic conditions]
>    "b" rdf:type xsd:string .
>    ...
> 
> I will use generalised RDF to make (my) life easier.
> 
> What we'll try to prove is that given:
> 
>    rdf:Property rdfs:subClassOf xsd:boolean . #AZ
> 
> the following triple must hold:
> 
>    "a" rdf:type rdf:Property .                #goal
> 
> since when it is combined with #AZ and rdfs9, it gives:
> 
>    "a" rdf:type xsd:boolean .
> 
> which should be D recognising-xsd:boolean-unsatisfiable.
> 
> ================================================================
> 
> We'll need some RDFS axiomatic triples:
> 
>    rdfs:domain rdfs:domain rdf:Property .        #A1
>    rdfs:range rdfs:domain rdf:Property .         #A2
>    rdfs:subPropertyOf rdfs:domain rdf:Property . #A3
>    rdf:type rdfs:range rdfs:Class .              #A4
>    rdf:type rdf:type rdf:Property .              #A5
> 
> ================================================================
> 
> Given:
> 
>    rdf:Property rdfs:subClassOf xsd:boolean .
> 
> We now have (at most) two possible "relations" in IP.
> 
> Per the pigeonhole principle, at least one pair here must refer to the 
> same property:
> 
>    rdf:type
>    rdfs:domain
>    rdfs:range
> 
> This leaves the following three cases.
> 
> ================================================================
> 
> Case 1: rdf:type and rdfs:domain refer to the same property.
> 
>    "a" rdfs:domain xsd:string .           #3 [#2 and Case 1]
>    "a" rdf:type rdf:Property .            #goal [#3, #A1 and rdfs2]
> 
> ================================================================
> 
> Case 2: rdf:type and rdfs:range refer to the same property.
> 
>    "a" rdfs:range xsd:string .            #4 [#2 and Case 2]
>    "a" rdf:type rdf:Property .            #goal [#4, #A2 and rdfs2]
> 
> ================================================================
> 
> Case 3: rdfs:domain and rdfs:range refer to the same property.
> 
>    rdf:type rdfs:domain rdfs:Class .      #5 [#A4 and Case 3]
>    "a" rdf:type rdf:Class .               #6 [#2, #5 and rdfs2]
>    "a" rdfs:subClassOf rdfs:Resource .    #7 [#6 and rdfs8]
> 
>   I don't see a good way to make direct progress from here, but within 
> Case 3, we can always invoke the pigeonhole principle again. At least 
> one pair here must refer to the same property:
> 
>    rdfs:domain/rdfs:range (already equivalent under Case 3)
>    rdfs:subClassOf
>    rdfs:subPropertyOf
> 
> This leaves three sub-cases.
> 
> ----------------------------------------------------------------
> 
> Case 3.1: rdfs:domain, rdfs:range and rdfs:subClassOf all refer to the 
> same property.
> 
>    "a" rdf:domain rdfs:Resource .         #8 [#7 and Case 3.1]
>    "a" rdf:type rdf:Property .            #goal [#8, #A1 and rdfs2]
> 
> ----------------------------------------------------------------
> 
> Case 3.2: rdfs:subClassOf and rdfs:subPropertyOf refer to the same 
> property.
> 
>    "a" rdfs:subPropertyOf rdfs:Resource . #9 [#7 and Case 3.2]
>    "a" rdf:type rdf:Property .            #goal [#9, #A3 and rdfs2]
> 
> ----------------------------------------------------------------
> 
> Case 3.3: rdfs:domain, rdfs:range and rdfs:subPropertyOf all refer to 
> the same property.
> 
> It will make (my) life easier to observe that within Case 3.3, either:
> 
> - Case 3.3.1: rdfs:subClassOf refers to the same property as 
> rdfs:domain, rdfs:range and rdfs:subPropertyOf, or
> - Case 3.3.2: rdfs:subClassOf refers to the same property as rdf:type.
> 
> Since Case 3.3.1 is covered by Case 3.2, we assume Case 3.3.2.
> 
>    rdf:type rdfs:subClassOf rdf:Property . #10 [#A5 and Case 3.3.2]
>    rdf:type rdfs:subPropertyOf rdf:type .  #11 [#A5 and rdfs6]
>    rdf:type rdfs:domain rdf:type .         #12 [#11 and Case 3.3]
>    "a" rdf:type rdf:type .                 #13 [#2, #12 and rdfs2]
>    "a" rdf:type rdf:Property .             #goal [#10, #13 and rdfs9]
> 
> ================================================================
> 
> In all cases given to us by the pigeons we infer the goal:
> 
>    "a" rdf:type rdf:Property .
> 
> Hence
> 
>    rdf:Property rdfs:subClassOf xsd:boolean .
> 
> ... is not RDFS-recognising {xsd:boolean}-consistent.
> 
> 
> So what's horribly complicated about that? :)
> 
> ================================================================
> 
> Disclaimer:
> 
> Possibly I made a mistake somewhere.
> 
> Possibly there is a much simpler argument.
> 
> Fun question for an exam!
> 

-- 
Antoine Zimmermann
Institut Henri Fayol
École des Mines de Saint-Étienne
158 cours Fauriel
CS 62362
42023 Saint-Étienne Cedex 2
France
Tél:+33(0)4 77 42 66 03
Fax:+33(0)4 77 42 66 66
http://www.emse.fr/~zimmermann/
Member of team Connected Intelligence, Laboratoire Hubert Curien