Issues in Semantic Web Logic

Dan Connolly

See also:

• The Semantic Web as a language of logic, in progress 199 by Tim Berners-Lee, part of the TimBL's Design Issues series

Motivating intuitions

• Motivations for the Web:
  1. help people work together at all scales, from individually to small groups to nations.
  2. exploit the power of computing in our every day lives
• State of the art (1998):
  • Computers help people send problem descriptions and solutions to each other
  • With fulltext search (aided by link structure), we can delegate much of the task of finding documents to the machine
  • Compute services can be exported over the web, black-box style
  • But when the airline sends me an itinerary, I have to manually copy and paste each field into my PDA
• Goal: integrate logic with Web protocols and data formats so that richer problems can be delegated to computers

The target: very expressive delegation

As written in 1998:

forall message,t, r, x, y (
  (signed(message,K)
    & derivable(t, message)
    & subject(t, x)
    & predicate(t, r)
    & object(t, y))
   -> r(x,y)
)

Flash Forward: Notation3 Trust

As implemented in ~2003:

{  [] acc:credential [ log:semantics :F ].
   :F log:includes { :str acc:endorsement[acc:signature :sig; acc:key :k]}.
   :k crypto:verify ([is crypto:md5 of :str] :sig).
   :str log:parsedAsN3 :G } log:implies { :G acc:certSupportedBy :k }.

cf. trust chapter of the SemWeb tutorial

Scalability trade-offs

Why do we think this is better than/different from "failed" AI efforts?

	Hypertext	Data/Logic
pre-web constraint	all links go both ways	every question can be answered yes/no by an effective decision procedure. Full understanding or bust*.
Web simplification	most links work; some links break; back-links are an optional extra	Any party can check a proof once one is found, but some questions take a long time or forever to answer. Partial understanding.
Web benefits	scalability: I can link from my private file to google/yahoo/cnn, without a link back from them	decentralized vocabulary development, ... increased expressivity?

*as characatured by Lenat at KT2001.

The Canonical Mathematical Logic: First Order Logic

cf. FOL in wikipedia

• syntax:
  1. terms: constants a, b, c; variables x, y, z; function applications f(a, g(x))
  2. atomic formulas: P(a, x, g(y))
  3. inductively defined formulas: for any formulas F and G, the following are fomulas not(F), F and G, F or G, if F then G, F iff G. For any formula F and variable x, All(x).F and Exists(x).F are formulas.
• complexity: semidecidable. resolution is sound and complete, may take forever to terminate
• important properties: compactness etc; cf section 3. Five grand theorems in Standford Encyclopedia entry

Innovation #1: Going Global with URIs in RDF

• URIs facilitate a global consensus about the meaning of symbols in 2 ways:
  1. URIs are cheap enough that if you see some URI used or "defined", and you intend to refer to something different, we can expect/require that you make up your own. Ambiguity from accidental re-use is a manageably small risk.
  2. When in doubt, follow your nose. Look it up.
• At first glance, these are entirely orthogonal to logic.
  But stay tuned for level-breaking features (log:uri) and integration with protocols (log:semantics)

RDF "graph" formulas

• A web link is a relationship between 2 URIs, v1, v2
• At least in theory, links have types; we'll use URIs for types too.
• A labelled graph edge { v1 r v2 } is like an atomic formula r(v1, v2)
  • but actually, more like holds(r, v1, v2)
• limitation: we don't have direct support for NaryRelations, i.e. relations of arity >2. in scope for a WG in the next year or so, I gather.
• A graph of these edges is a conjunction
• Literals (strings, numbers... )are also allowed as terms
• Existentials are also allowed as terms
  • Inference (erasure and existential introduction) is as hard as subgraph matching on partially labelled graphs (n-p complete, I think)

Reification and quoting

• If you feed this to cwm:

  :lois :believes [
    rdf:subject :clark;
    rdf:predicate rdf:type;
    rdf:object :Wimp ].
  :clark = :superman.
  { ?O1 = ?O2. ?S ?P ?O1 } => { ?S ?P ?O2 }.
  

  and ask it to --think, then it will conclude that lois thinks that superman is a wimp too:

  :lois :believes [
    rdf:subject :clark, :superman;
    rdf:predicate rdf:type;
    rdf:object :Wimp ].
  

• but if you feed this to cwm:

  :lois :believes { :clark rdf:type :Wimp }.
  :clark = :superman.
  { ?S1 = ?S2. ?S1 ?P ?O } => { ?S2 ?P ?O }.
  

  and ask it to think, it won't find any new conclusions. The occurrence of :clark within { :clark rdf:type :Wimp } is quoted.

cf reification tests in 0.8 release, proof ontology...

Self-reference, Negation and the Liar's paradox

• recall we're interested in quoting:
  { ?F log:or ?G. ?F a log:Falsehood } => { ?G a log:Truth }
• formula self-reference:

  { this a log:Falsehood }
  

• document self-reference:

       <>.log:semantics a log:Falsehood.
     

• loops:

  in <A>:

  <B>.log:semantics a log:Truth

  in <B>:

  <A>.log:semantics a log:Falsehood

Russel's Paradox

_:a rdf:type daml:Restriction .
_:a daml:onProperty rdf:type .
_:a daml:maxCardinalityQ 0 .
_:a daml:hasClassQ _:b .
_:b daml:oneOf _:c .
_:c daml:first _:a .
_:c daml:rest daml:nil . 

cf From KL-ONE to OWL: Description Logics in the Ivory Tower and the Semantic Web by Peter F. Patel-Schneider

Scalability and the law of the excluded middle

Suppose we drop the P \/ not(P) constraint from FOL?

In the world of metamathematics, the intuitionists are not at all exotic, despite the centrality of the PEDC (hence the PEM) to the ordinary sense of consistency. Their opponents do not scorn them as irrationalists but, if anything, pity them for the scruples that do not permit them to enjoy some "perfectly good" mathematics.

Non-Contradiction and Excluded Middle in Peter Suber's Logical Systems course notes

We lose DeMorgan's laws and such, but it seems like it should work. It's a well-trodden path (see Isabelle.

@@more

• PCA, Guha's contexts, ... refs