- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Tue, 21 May 2002 16:14:15 +0200
- To: pfps@research.bell-labs.com
- Cc: "www-webont-wg" <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 see & agree as said last night, we have it that the consequent of an asserted implication can't be not() or not(s) so our stuff is incomplete (but consistent I hope) -- Jos
Received on Tuesday, 21 May 2002 11:04:48 UTC