Simple Conditionals(An RDF Logic)

Status

$Revision: 1.5 $ $Date: 2002/05/01 20:12:00 $

previous proposal, which had problems with RDF entailment.

A proposal and issues discussion.

ToDo: actually write the DAML+OIL Ontology for this, in addition to the inference tools.

Introduction

We want some kind of inference system on the Semantic Web to make managing vast quantities of facts easier. Simple classification schemes like RDF Schema and much more complex Description Logics like DAML+OIL are nice, but I happen to like if-then statements. Sometimes they are called "rules", and they are very much like Prolog rules, but I mean them in the declarative sense. If you had knowledge that a consequent was false, it would be correct to infer that an antecedent was false; however, we have no notion of falseness here.

I want a logic that's simple and close to (my view of) the spirit of RDF and the semantic web. This work is very similar to TimBL's logic in cwm, except..., well, I think this is simpler. He started with the idea of doing FOL, I think, and then dropped down to the same expressive power as I'm using here. But at this level, I don't think we really need to introduce formulas.

Example 1

Informally: If Sandro is in his study, then Sandro is in his house

  @prefix rdf:  .
  @prefix xlog:  .
  [ a xlog:Conditional;
    xlog:exiVars ();
    xlog:uniVars ();
    xlog:if ([ rdf:subject sandro:sandro; rdf:predicate sandro:location; rdf:object sandro:myStudy ]);
    xlog:then ([  rdf:subject sandro:sandro; rdf:predicate sandro:location; rdf:object sandro:myHouse ]);
  ].

Example 2

Here's an example which implements rdfs:subClassOf using this example logic.

Informally: if INSTANCE has rdf:type SUBCLASS, and SUBCLASS is a subclass of SUPERCLASS, then INSTANCE also has rdf:type SUPERCLASS.

  @prefix rdf:  .
  @prefix xlog:  .
  [ a xlog:Conditional;
    xlog:exiVars ();
    xlog:uniVars (:INSTANCE :SUBCLASS :SUPERCLASS);
    xlog:if (
       [ rdf:subject :INSTANCE; rdf:predicate rdf:type; rdf:object :SUBCLASS ];
       [ rdf:subject :SUBCLASS; rdf:predicate rdfs:subclassOf;
  rdf:object :SUPERCLASS ]
    );
    xlog:then ([  rdf:subject :INSTANCE; rdf:predicate rdf:type; rdf:object :SUPERCLASS ]);
  ].

Issues

Why (Conjunction Consequents and ExiVars) instead of Logic Functions

In Horn clauses, you have neither multiple consequents nor existentially quantified variables, but this seems (intuitively) to have the same expressive power. It's because we don't have logic functions, so we can't convert existentials it Skolem functions. In fact, an implementation is going to have to do something similar to functions internally to handle this, but.... Why not functions? Too unlike RDF.

Why Use DAML Lists & Unique Properties

The idea here is to say an RDF Graph which contains a described Conditional may entail (in this simple-conditional logic) some additional statements described in the Conditional. Unfortunately, RDF entailment makes it valid to just drop some arcs from the graph, which could change the conditional (if specified in the more obvious way) into simply asserting the consequents. In other words, RDF-entailment plus simple-conditional entailment turns the other style Conditionals into mere assertions, entirely losing their intended meaning.

Terminology

The terms log:antecedent and log:consequent would be more accurate, but they are too long.

I have no idea what to call this logic, or what prefix to use for it. Using "log:" is probably a bad idea.

Quantification Semantics

@@@@

Like cwm logic when you don't treat log:forAll as an n3 keyword, we're using objects in the domain of discourse as variables. We're doing it in a more constrained form -- the substitutions allowed are only in the if and then clauses, not in the places where the forSome and forAll are. That helps a little.

Here's the glitch: in example 2, we don't know if the denotations of rdf:type and :INSTANCE are the same. If they were, then rdf:type would also be a variable in that rule.

Solution: until/unless you learn they are the same, assume they are not. Learning they are the same is a lot like learning rdf:type is declared log:forAll. It changes what can be inferred, and that's fine. If you knew they were the same, doing a textual substitution would seem okay, and it would turn out to be okay.

The alternative would be to add a layer of indirection, where the rdfx:subject is a logical constant or a logical variable, etc, like I did with my layering of FOL on RDF.

Inferring more Conditionals

@@@

What if a log:then clause causes another Conditional to be described? You really should recognize and use it. This makes things rather messy for Prolog; we'll need an outer wrapper, I think. So be it.

Some cases, maybe all, can be handled by static analysis. A=>(B=>C) === (A & B) => C (and keep the original around, because you still need to infer the cruft -- but you don't need to recognize anything from it, since you kind of already did.

(Desired) Tools

* Compute the deductive closure, using this inference.

* Query the deductive closure; provide proofs for each solution.

* Convert cwm-think's vocab to this (via these rules)

* Convert pure prolog to this; convert this to pure prolog ?

These kind of need to interoperate with other vocabularies....

Sandro Hawke
First: 2002-03-29; This: $Id: conditional.html,v 1.5 2002/05/01 20:12:00 sandro Exp $