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.