- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 15 Apr 2004 12:00:17 -0500
- To: Jeremy Carroll <jjc@hpl.hp.com>
- Cc: www-archive+n3bugs@w3.org, Tim Berners-Lee <timbl@w3.org>, www-rdf-logic@w3.org, public-cwm-bugs@w3.org
On Wed, 2004-04-14 at 02:12, Jeremy Carroll wrote: > Hi Tim, Dan, > > apologies for rather formal tone here, I think it may be clearer than an > informal tone. This is essentially a bug report with suggested fix. > I suspect it is of wider interest, hence the www-rdf-logic CC. Makes sense to me, but I can't speak for TimBL with confidence here. I hope he'll respond in due course. > This is a comment on: > > http://www.w3.org/2000/10/swap/log > > Summary: > > If this vocab is understood as logical rather than proof theoretic then it is > inconsistent. Suggest changing rdfs:comments to prioritise proof theoretic > reading. > > A few sample suggested changes: > > OLD > log:Truth a rdfs:Class; > rdfs:comment """Something which is true: belive it as you would belive > this. > Understood natively by cwm in that it will execute rules in a formula > declared a Truth within a formula it is already taking rules > from.""". > > NEW > log:Truth a rdfs:Class; > rdfs:comment """Something which is provable or axiomatically true: > believe it as you would believe this. > Understood natively by cwm in that it will execute rules in a formula > declared a Truth within a formula it is already taking rules > from.""". > > > OLD: > > log:implies a rdf:Property; > rdfs:comment """Logical implication. > This is the relation between the antecedent (subject) and > conclusion (object) of a rule. > For every subsitution of variable names for symbols or literals > which maps the antecedent to a fromula which knowledge base > log:includes, the same substitution is applied to the > conclusion to generate the result. > > Used by cwm as the basic hook for adding inference to RDF. > See the manual to define what the knowledge base is and > where the results go. See also log:conclusion."""; > > NEW > > > log:implies a rdf:Property; > rdfs:comment """The provability relationship. > This is the relation between the antecedent (subject) and > conclusion (object) of a rule. > For every subsitution of variable names for symbols or literals > which maps the antecedent to a fromula which knowledge base > log:includes, the same substitution is applied to the > conclusion to generate the result. > > Used by cwm as the basic hook for adding inference to RDF. > See the manual to define what the knowledge base is and > where the results go. See also log:conclusion."""; > > > ============ > > Rationale. It is possible to use rdfs:comment to introduce a contradiction > when the comment is understood as constraining the class or property (as is > the intent). e.g. > > eg:Russell a rdfs:Class; > rdfs:comment """The class of all classes that do not have themselves as a > type. i.e. ?x a eg:Russell if and only if not ?x a ?x""" . > > This appears to be just normal RDF (no N3 extensions), but is seriously > flawed. There are no interpretations for which the comment, understood in > English, describes the class eg:Russell. > > Similarly the current description of log:implies as "Logical implication" is > flawed since there are no interpretations that make it true as shown by the > liar paradox that I posted earlier: > http://lists.w3.org/Archives/Public/www-rdf-logic/2003Nov/0040 > > @prefix log: <http://www.w3.org/2000/10/swap/log#> . > @prefix owl: <http://www.w3.org/2002/07/owl#> . > { > <http://example.org/liar> > log:implies { > <http://example.org/noone> a owl:Nothing . > } . > } owl:sameAs <http://example.org/liar> . > <http://example.org/liar> a log:Truth . > > See also Pat's posting on the rules list: > http://lists.w3.org/Archives/Public/www-rdf-rules/2002Dec/0003 > > A better fix would be to whole-heartedly embrace proof theoretic and define > these terms using an abstract proof theory rather than a concrete proof > machine (CWM). i.e. I see text like: > """Used by cwm as the basic hook for adding inference to RDF. > See the manual to define what the knowledge base is and > where the results go. See also log:conclusion.""" > as essentially OK, and a good foundation on which to build a more abstract > definition of a proof theoretic nature: log:implies is essentially practical > not logical. > > Jeremy > > > -- Dan Connolly, W3C http://www.w3.org/People/Connolly/ see you at the WWW2004 in NY 17-22 May?
Received on Thursday, 15 April 2004 12:59:34 UTC