- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Wed, 14 Apr 2004 09:12:53 +0200
- To: www-archive+n3bugs@w3.org, timbl@w3.org, connolly@w3.org
- Cc: www-rdf-logic@w3.org
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. 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
Received on Wednesday, 14 April 2004 03:14:37 UTC