Toward proof exchange in the Semantic Web

Dan Connolly

Decentralized Information Group
MIT Computer Science and Artificial Intelligence Laboratory

Policy Aware Web (PAW) Project

• Abstract:

  In this paper, we describe the motivations for, and development of, a rule-based policy management system that can be deployed in the open and distributed milieu of the World Wide Web. We discuss the necessary features of such a system in creating a "Policy Aware" infrastructure for the Web, and argue for the necessity of such infrastructure. We then show how the integration of a Semantic Web rules language (N3) with a theorem prover designed for the Web (Cwm) makes it is possible to use the Hypertext Transport Protocol (HTTP) to provide a scalable mechanism for the exchange of rules and, eventually proofs, for access control on the Web. We also discuss which aspects of the Policy Aware Web are enabled by the current mechanism and describe future research needed to make the widespread deployment of rules and proofs on the Web a reality.

  Daniel Weitzner, Jim Hendler, Tim Berners-Lee, and Dan Connolly. Creating a policy-aware web: Discretionary, rule-based access for the world wide web. In Elena Ferrari and Bhavani Thuraisingham, editors, Web and Information Security. IRM Press, 2006.

• A collaboration between the University of Maryland Mindswap (Hendler, ...) and DIG (Weitzner, Berners-Lee, Connolly, ... )
• policyawareweb.org
• Funded under NSF ITR 04-012

A PAW scenario: access to girl scout event photos

Current working some PAW examples include:

The troop policy is:

1. Photos taken at meetings of the troop can be shared with any current member of the troop.
2. Photos taken at a jamboree can be shared with anyone in the troop or with anyone who attended the jamboree.
3. Photos of the girls winning awards can be shared with anyone currently in the troop, or who was ever a member. These award photos can also be shared with the public if, and only if, the girl's parents allow it.

For more, see:

• Lalana Kagal, Tim Berners-Lee, Dan Connolly, and Daniel Weitzner, Using Semantic Web Technologies for Open Policy Management on the Web, 21st National Conference on Artificial Intelligence (AAAI 2006), with talk slides

Transparent Accountable Datamining Initiative (TAMI) Project

• The TAMI Project is creating technical, legal, and policy foundations for transparency and accountability in large-scale aggregation and inferencing across heterogeneous information systems. The incorporation of transparency and accountability into decentralized systems such as the Web is critical to help society manage the privacy risks arising from the explosive progress in communications, storage, and search technology. The expansion of government use of large-scale data mining for law enforcement and national security provides a compelling motivation for this work. While other investigations of the impact of data mining on privacy focus on limiting access to data as a means of protecting privacy, a variety of social, political, and technical factors are making it increasingly difficult to limit collection of and access to personal information. The TAMI Project is addressing the risks to privacy protection and the reliability of conclusions drawn from increasing ease of data aggregation from multiple sources by creating methods and technologies for adding increased transparency and accountability of the inferencing and aggregation process itself. The project is developing precise rule languages that are able to express policy constraints and reasoning engines that are able to describe the results they produce.

• Weitzner, Abelson, Berners-Lee, Hanson, Hendler, Kagal, McGuinness, Sussman, Waterman, Transparent Accountable Data Mining: New Strategies for Privacy Protection,; MIT CSAIL Technical Report MIT-CSAIL-TR-2006-007
• working with InferenceWeb project (McGuiness, ...) at Stanford
• supported by the US National Science Foundation Cybertrust (05-518) program.
• ... TAMI web page

A TAMI scenario:

Adverse actions premised on inferences from data where the data, while factually correct and properly in possession of the user, is used for an impermissible purpose.

TSA finds a possible name match (of a very common name) between a person in a Passenger Name Record and a person in the Terrorist Screening DataBase and properly sends the information to the FBI. The FBI arrests him for unpaid child support under the federal "Deadbeat Dad" statute. This will turn out to be impermissible because:

1. the SORN says the purpose of collecting Passenger Name Record information is "to enhance the security of domestic air travel by identifying only those passengers who warrant further scrutiny" and
2. the Privacy Act requires USPerson data to be used only for the purposes for which it was collected.

Semantic Web Basics

• What is the Semantic Web?
  • Data integration across application, organizational boundaries
• How does it work?
  1. Apply power of URIs to concepts of relational data
     • Don't say "colour" say <http://example.com/2002/std6#col>
  2. Model real things, not just documents or database tables

Logic, Databases, and Scale

Are there parts of traditional logic and databases that, if we set them aside, will result in viral growth of the Semantic Web?

Semantic Web standards and research

Berners-Lee, Jan 2003

Semantic Web Atomic Formulas

• The Resource Description Framework (RDF)
  • abstract syntax, formal semantics
  • standard encoding in XML
  • emerging programmer-friendly short-hand encoding: N3/turtle

Note the relationship to HTML links, especially with the re-discovery of the rel attribute in microformats: vote-for, friend, etc..

Semantic web includes tables, trees...

... and tangly messes

RDF Terms: URIs, literals, existentials

• string literals, integer literals:

  MyConf conf:eventName "WWW2006 Workshop on Models of Trust for the Web".
  MyConf conf:numOfRegistrants 65.
  

• existentials:

    @forSome X. j:Joe foaf:knows X. X foaf:name "Fred" .
  
    j:Joe foaf:knows [ foaf:name "Fred" ] .
  

• The Twelfth International World Wide Web Conference, Budapest HUNGARY, May 2003; Semantic Web Tutorial Using N3 with Sandro Hawke and Tim Berners-Lee
• Dave Beckett, Turtle - Terse RDF Triple Language, work in progress 2004-2006

  This is an N3 subset that corresponds to the RDF/XML standard.

RDFS and OWL Standards

RDF Schema (RDFS) and the Web Ontology Language (OWL) correspond to UML notions such as subclass, domain, range, cardinality, etc.

• cyc terms in red
• DAML airport ontology terms in purple
• custom travelTerms in green.
• RDF standard terms in blue
• XML Schema terms in orange

SQL * URIs = SPARQL

Aggregate data from friends etc, then...

  PREFIX foaf: <http://xmlns.com/foaf/0.1/>
  PREFIX c: <http://www.w3.org/2002/12/cal/icaltzd#>
  SELECT ?name, ?summary, ?when
   FROM <myFriendsBlogsData>
   WHERE { ?somebody foaf:name ?name; foaf:mbox ?mbox.
           ?event c:summary ?summary;
                  c:dtstart ?ymd;
                  c:attendee [ c:calAddress ?mbox ]
         }.

See SPARQL Query Language for RDF W3C Working Draft 21 July 2005

N3 Rules

@keywords is, of, a.
@prefix : <#>.

socrates a Man.
{ ?who a Man } => { ?who a Mortal }.

Reminder: we're using URIs

socrates a Man.

abbreviates

<#socrates> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <#Man>.

Standard terms for idioms

We can say this much using just the RDF/RDFS standards:

socrates a Man.
Man rdfs:subClassOf Mortal.

And then we can implement the standard RDFS semantics with rules:

@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

{ ?X a [rdfs:subClassOf ?C] } => { ?X a ?C }.

A proof

• python cwm.py socrates.n3 --think --why >socrates-pf.n3
• python check.py socrates.n3 socrates-pf.n3

  1: ... [by parsing <socrates.n3>]
  
  2: :socrates a :Man .
   [by CE on 1]
  
  3: @forAll :who . { :who a :Man . } log:implies {:who a :Mortal . } .
   [by CE on 1]
  
  4: ...
   [by GMP on 3, [2]]
  
  5: @forAll :who . :socrates a :Man, :Mortal . { :who a :Man . } log:implies {:who a :Mortal . } .
   [by CI on [1, 4]]
  

Using web access and quoting to express policies

• Policy: if someone's home page says that they are a vegetarian, then we believe that they are a vegetarian.

• @prefix foaf: <http://xmlns.com/foaf/0.1/>.
  @prefix log: <http://www.w3.org/2000/10/swap/log#> .
  
  @forAll WHO.
  
  { WHO foaf:homepage ?PG.
   ?PG log:semantics [ log:includes { WHO a Vegetarian } ]
  } => { WHO a Vegetarian}.
  

Expressing policies (cont)

• Conference organizers set up conf_reg_ex.n3:

  @forAll WHO.
  
  { WHO foaf:homepage ?PG.
   ?PG log:semantics [ log:includes { WHO a Vegetarian } ]
  } => { WHO a Vegetarian}.
  
  <joe_profile.n3#joe> foaf:homepage <joe_profile.n3>.
  

• Joe writes, in joe_profile.n3:

  <#joe> foaf:homepage <>; a Vegetarian.
  

A proof using the Vegetarian policy

• python cwm.py conf_reg_ex.n3 --think --why >,veg-pf.n3
• python check.py ,veg-pf.n3

  1: ...
   [by parsing <conf_reg_ex.n3>]
  
  2: :joe <http://xmlns.com/foaf/0.1/homepage> <file:/Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3> .
   [by CE on 1]
  
  3: <file:/Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3> log:semantics {joe:joe a :Vegetarian; <http://xmlns.com/foaf/0.1/homepage> <file:/Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3> . } .
   [by built-in Axiom log:semantics]
  
  4: { joe:joe a :Vegetarian; <http://xmlns.com/foaf/0.1/homepage> <file:/Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3> . } log:includes {joe:joe a :Vegetarian . } .
   [by built-in Axiom log:includes]
  
  5: @forAll :WHO, con:PG . { @forSome foo:_g3 . foo:_g3 log:includes {:WHO a :Vegetarian . } . :WHO <http://xmlns.com/foaf/0.1/homepage> con:PG . con:PG log:semantics foo:_g3 . } log:implies {:WHO a :Vegetarian . } .
   [by CE on 1]
  
  6: ...
   [by GMP on 5, [2, 3, 4, 4]]
  
  7: @forAll :WHO, con:PG . joe:joe a :Vegetarian; <http://xmlns.com/foaf/0.1/homepage> <file:/Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3> . { @forSome foo:_g3 . foo:_g3 log:includes {:WHO a :Vegetarian . } . :WHO <http://xmlns.com/foaf/0.1/homepage> con:PG . con:PG log:semantics foo:_g3 . } log:implies {:WHO a :Vegetarian . } .
   [by CI on [1, 6]]
  

Related Work

• InferenceWeb's proof browser can browse these proofs, using a conversion to PML
• Jos DeRoo's Euler backward-chainer produces proofs that interoperate with chek.py
• log:semantics is similar to the knowledge function, K, in
  • Z. Pan and A. Qasem and J. Heflin An Investigation into the Feasibility of the Semantic Web. In Proc. of the Twenty First National Conference on Artificial Intelligence (AAAI 2006), Boston, USA, 2006 (abstract)