- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Mon, 20 May 2002 15:31:51 -0400
- To: jos.deroo.jd@belgium.agfa.com
- Cc: www-webont-wg@w3.org
This example uses a natural deduction-style proof system.
Additional axioms
Axioms about the Russell set:
a/ ?x a :R -> ?x a [ owl:complementOf ?x ]
b/ ?x a [ owl:complementOf ?x ] -> ?x a :R
Axioms about complementOf:
c/ ?x a [ owl:complementOf ?y ] -> not ( ?x a ?y )
d/ not ( ?x a ?y ) -> ?x a [ owl:complementOf ?y ]
Proof:
| :R a :R Assumption
|--------
| :R a :R -> :R a [ owl:complementOf :R ] a/ (universal elimination)
|
| :R a [owl:complementOf ?x] -> elimination
|
| :R a [owl:complementOf :R] -> not(:R a :R ) c/ (universal elimination)
|
| not(:R a :R) -> elimination
|
| FALSE not elimination
not(:R a :R) not introduction
| not(:R a :R) Assumption
|-------------
| not ( :R a :R ) -> :R a [owl:complementOf :R] d/ (universal elimination)
|
| :R a [ owl:complementOf :R ] -> elimination
|
| :R a [ owl:complementOf :R ] -> :R a :R b/ (universal elimination)
|
| :R a :R -> elimination
|
| FALSE not elimination
not(not(:R a :R)) not introduction
FALSE not elimination
Received on Monday, 20 May 2002 15:33:16 UTC