Issues in Semantic Web Logic

Dan Connolly
MIT 6.898 - Notions & Notations of the Semantic Web
20 Oct 2005

See also:

$Revision: 1.5 $ of $Date: 2005/10/20 15:08:55 $

Motivating intuitions

The target: very expressive delegation

As written in 1998:

forall message,t, r, x, y (
    & 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

Innovation #1: Going Global with URIs in RDF

RDF "graph" formulas

Reification and quoting

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

Self-reference, Negation and the Liar's paradox

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.