SHOW:
|
|
- or go back to the newest paste.
| 1 | - | Given: |
| 1 | + | |
| 2 | Though.. lets use a skolem: | |
| 3 | ||
| 4 | fact1- i:myCar rdf:type c:HondaCivic . | |
| 5 | fact2- c:HondaCivic rdfs:subClassOf c:PassengerVehicle . | |
| 6 | fact3- c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured . | |
| 7 | - | From fact1 + fact2 + fact3 may i conclude? |
| 7 | + | rule1- (forall ?i ?c ?se { ?c rdfs:subClassOf ?sc. ?i rdf:type ?c . }) -> (exists ?r { ?r rdfs:subProperty rdf:type }-> {?i ?r ?sc. }).
|
| 8 | ||
| 9 | - | result1- i:myCar rdf:type c:PassengerVehicle . |
| 9 | + | |
| 10 | - | result2- i:myCar rdf:type c:ThingThatCanBeInsured . |
| 10 | + | result1> ?WHAT = c:PassengerVehicle, |
| 11 | ||
| 12 | - | No, because FOL doesnt give me this transitive closure . |
| 12 | + | |
| 13 | rule1- (forall ?i ?c ?se { ?c rdfs:subClassOf ?sc. ?i rdf:type ?c . }) -> (exists ?r { ?r rdfs:subProperty rdf:type }-> {?i ?r ?sc. }).
| |
| 14 | - | So, Lets make it by adding a rule: |
| 14 | + | |
| 15 | fact2- c:HondaCivic rdfs:subClassOf c:PassengerVehicle . | |
| 16 | - | rule1 - { ?c rdfs:subClassOf ?sc. ?i rdf:type ?c . } -> { ?i rdf:type ?sc }
|
| 16 | + | ded1- { _:R+ rdfs:subProperty rdf:type } -> {i:myCar _:R+ c:PassengerVehicle . }).
|
| 17 | ded2- { _:R_{i:myCar rdf:type c:HondaCivic, c:HondaCivic rdfs:subClassOf c:PassengerVehicle} rdfs:subProperty rdf:type }
| |
| 18 | ded3- { i:myCar _:R+{i:myCar rdf:type c:HondaCivic, c:HondaCivic rdfs:subClassOf c:PassengerVehicle} c:PassengerVehicle }
| |
| 19 | ded4- -> i:myCar _:R+ c:PassengerVehicle | |
| 20 | - | ASK> i:myCar rdf:type ?WHAT |
| 20 | + | |
| 21 | ||
| 22 | result2> ?WHAT = c:ThingThatCanBeInsured, | |
| 23 | - | result1> ?WHAT = c:PassengerVehicle |
| 23 | + | |
| 24 | proof> | |
| 25 | - | rule1- { ?c rdfs:subClassOf ?sc. ?i rdf:type ?c . } -> { ?i rdf:type ?sc }
|
| 25 | + | rule1- (forall ?i ?c ?se { ?c rdfs:subClassOf ?sc. ?i rdf:type ?c . }) -> (exists ?r { ?r rdfs:subProperty rdf:type }-> {?i ?r ?sc. }).
|
| 26 | fact1- i:myCar rdf:type c:HondaCivic . | |
| 27 | fact2- c:HondaCivic rdfs:subClassOf c:PassengerVehicle . | |
| 28 | - | rule1+fact2+fact1 c:HondaCivic rdfs:subClassOf c:PassengerVehicle . i:myCar rdf:type c:HondaCivic . |
| 28 | + | ded1- { _:R+ rdfs:subProperty rdf:type } -> {i:myCar _:R+ c:ThingThatCanBeInsured }).
|
| 29 | - | ded1- -> i:myCar rdf:type c:PassengerVehicle |
| 29 | + | ded2- { _:R+{i:myCar rdf:type c:HondaCivic, c:HondaCivic rdfs:subClassOf c:PassengerVehicle, c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured} rdfs:subProperty rdf:type }
|
| 30 | ded3- -> { i:myCar _:R+{i:myCar rdf:type c:HondaCivic, c:HondaCivic rdfs:subClassOf c:PassengerVehicle, c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured} c:ThingThatCanBeInsured }
| |
| 31 | - | result2> ?WHAT = c:ThingThatCanBeInsured |
| 31 | + | ded4- -> i:myCar _:R+ c:ThingThatCanBeInsured |
