Inference Rules =============== 1. C and D 2(1,C). C 3(1,C). D 1. C or D 2a(1,D). C 2b(1,D). D 1. not not C 2(1,NE). C 1. C SubClassOf D 2a(1,I). not C 2b(1,I). D 1. C EquivalentTo D 2(1,EQ). C SubClassOf D 3(1,EQ). D SubClassOf C 1. not (C and D) 2a(1,DM). not C 2b(1,DM). not D 1. not (C or D) 2(1,DM). not C 3(1,DM). not D 1. C SubClassOf (p some D) 2a(1,QE). not C(a) or ( p(a,sk1) and D(sk1) ) where a is any instance of your choice and sk1 is a Skolem instance, ie, a new instance that does not appear previously. The existential quantification description can also be on the left-hand side of the implication: 1. (p some D) SubClassOf C 2a(1,QE). not p(a,sk1) or not D(sk1) or C(a) where a is any instance of your choice and sk1 is a Skolem instance, ie, a new instance that does not appear previously. In the following examples of QE application only the first form is given (existential quantification on the right-hand side). From the above, you can easily see how the rule would apply for the other form as well (existential quantification on the left-hand side). 1. C SubClassOf (p min 2 D) 2a(1,QE). not C(a) or ( p(a,sk1) and p(a,sk2) and D(sk1) and D(sk2) and not (sk1==sk2) ) where a is any instance of your choice and sk1, sk2 and Skolem instances, ie, new instances that do not appear previously. Similarly for any number used in the existential restriction. 1. C SubClassOf (p max 2 D) 2a(1,QE). not C(a) or not p(a,sk1) or not p(a,sk2) or not p(a,sk3) or not D(sk1) or not D(sk2) or not D(sk3) or sk1==sk2 or sk1==sk3 or sk2==sk3 where a is any instance of your choice and sk1, sk2 and Skolem instances, ie, new instances that do not appear previously. Similarly for any number used in the existential restriction. 1. C SubClassOf (p min 2 D) 2a(1,QE). not C(a) or ( p(a,sk1) and p(a,sk2) and D(sk1) and D(sk2) and not (sk1=sk2) ) where a is any instance of your choice and sk1, sk2 and Skolem instances, ie, new instances that do not appear previously. Similarly for any number used in the existential restriction. 1. C SubClassOf (p all D) 2(1,QU). not C(a) or not p(a,b) or D(b) where a and b are any instances of your choice. 1. (p all D) SubClassOf C 2(1,QU). ( p(a,b) and not D(b) ) or C(a) where a and b are any instances of your choice. 1. Transitive: p 2. p(a,b) 3. p(b,c) 4(1,2,3,T). p(a,c) 1. Symmetric: p 2. p(a,b) 3(1,2,S): p(b,a) EXAMPLE 1 ========= If something is a Big Building, then it must have at least 2 parts that are Big Rooms: 1. (Building and Big) subClassOf hasPart min 2 (Big and Room) Nothing can be Big and a Small at the same time: 2. Big subClassOf not Small 3. Small subClassOf not Big The partOf relation is transitive 4. Transitive: partOf An instance of a building, its appartments, and their rooms 5. Building(b1) 6. Appartment(a1) 7. partOf(a1,b1) 8. (Big and Room)(r1) 9. partOf(r1,a1) 10. Appartment(a2) 11. partOf(a2,b1) 14. (Small and Room)(r2) 15. partOf(r2,a2) There are no other Rooms in this universe: 16. Room subClassOf {r1,r2} (In actual usage we would locally close the parts of b1: 16. (partOf all {a1,a2,r1,r2})(b1) but since we only have one building in our universe, let us not worry about this for now) We can prove that b1 is not Big as follows: 17. Big(b1) 18(1,QE). not Building(b1) or not Big(b1) or ( partOf(b1,sk1) and partOf(b1,sk2) and (Big and Room)(sk1) and (Big and Room)(sk2) and not (sk1==sk2) ) 19a(17,D). not Building(b1) CLOSED(5) 19b(17,D). not Big(b1) CLOSED(17) 19c(17,D). partOf(b1,sk1) and partOf(b1,sk2) and (Big and Room)(sk1) and (Big and Room)(sk2) and not (sk1==sk2) 20(19c,C). partOf(b1,sk1) 21(19c,C). partOf(b1,sk2) 22(19c,C). Big(sk1) 23(19c,C). Room(sk1) 24(19c,C). Big(sk2) 25(19c,C). Room(sk2) 26(19c,C). not (sk1==sk2) 27(14,C). Room(r2) 28(14,C). Small(r2) 29(3,QU). not Small(r2) or not Big(r2) 30a(29,D). not Big(r2) 30b(29,D). not Small(r2) CLOSED(28) 31(16,QU). not Room(sk1) or {r1,r2}(sk1) 32a(31,D). {r1,r2}(sk1) 32b(31,D). not Room(sk1) CLOSED(23) 33a(32a,D). sk1 == r1 34b(32a,D). sk1 == r2 35b(30a,33b,=). not Big(sk1) CLOSED(22) 34a(16,QU). not Room(sk2) or {r1,r2}(sk) 35aa(34a,D). {r1,r2}(sk2) 35ab(34a,D). not Room(sk2) CLOSED(25) 36aa(35aa,D). sk2 == r1 36ab(36aa,D). sk2 == r2 37ab(30a,36ab,==). not Big(sk2) CLOSED(24) 37(33a,36aa,==). sk1 == sk2 CLOSED (26) Observe that the only axioms we needed for the equality operator are symmetry and transitivity, which are expressible as logic propositions. In other words, there is nothing special about '==' except the infix syntax, and the same proof could have derived using an 'equals' relation without the special syntax we usually reserve for equality. Observe also that partOf was not used. Semantically, since there is only one (Big and Room) in this universe, it is not necessary to check the parts of b1 to decide that b1 cannot be Big. Let us amend 16 as follows: 16. Room subClassOf {r1,r2,r3} There is now a third room, which might be Big and which might be part of b1. We expect Big(b1) to be consistent but not valid.