# Accepts data.ttl and background.ttl as input

# $Author: lkagal $
# $Date: 2006-07-15 22:33:03 -0400 (Sat, 15 Jul 2006) $
# $Revision: 1356 $

# USAGE: cwm http://dig.csail.mit.edu/TAMI/cph/v2/data.ttl http://dig.csail.mit.edu/TAMI/cph/v2/background.ttl rules-0715.n3 --think  --filter="min-filter-0715.n3"

# USAGE: cwm http://dig.csail.mit.edu/TAMI/cph/v2/data.ttl http://dig.csail.mit.edu/TAMI/cph/v2/background.ttl rules-0715.n3 --think  --filter="min-filter-0715.n3" --base=foo --why=n > scenario3.proof


@keywords a.

@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix dc: <http://purl.org/dc/elements/1.1/> .

@prefix log: <http://www.w3.org/2000/10/swap/log#> .

@prefix u: <http://niem.gov/niem/universal/0.3#>.
@prefix c: <http://niem.gov/niem/common/0.3#>.
@prefix j: <http://www.niem.gov/niem/domains/justice/0.3#>.

@prefix ts: <http://dig.csail.mit.edu/TAMI/data-schema#> .
@prefix tb: <http://dig.csail.mit.edu/TAMI/background#> .
@prefix law: <http://dig.csail.mit.edu/TAMI/law/> .

@prefix : <http://dig.csail.mit.edu/TAMI/lkagal/scenario3/rules#> .

@forAll X, Y.
@forAll P, A, C, R, S.

# identifying proof tree
{ X a j:Arrest.
} => { X a ProofNode }.

{ X a ProofNode.
  X ts:antecedent Y.
} => { Y a ProofNode }.

{ X a ProofNode; ts:antecedent tb:no-antecedent.
} => { X a RootNode }.

# if in RootNode data is being transferred to SOR
# then purposes intersect with purposes of applicable SORN
{ X a ProofNode.
  X ts:purpose P; ts:recipient R.
  R ts:notice S.
  S a ts:SORN; ts:purpose P.
} => { X sorn S; purpose P; recipient R }.

# if data is being transferred out of SOR
# then intersect with purposes of routine use 
{ X a ProofNode.
  X ts:purpose P; ts:source R; ts:antecedent Y.
  R ts:notice S.
  S a ts:SORN; ts:routineUse [ ts:purpose P ].
} => { X purpose P; source R }.

# if transaction has no purpose, then it retains the purpose of its antecedent
{ X a ProofNode; purpose P.
  Y ts:antecedent X.
  Y ts:purpose tb:any-purpose.
} => { Y purpose P }.

# a proof node is a purpose node, if it has a non empty purpose and all its antecedents 
# have non empty purposes
{ X a RootNode; purpose P.
} => { X a NonEmptyPurposeNode }.

{ X a NonEmptyPurposeNode.
  Y ts:antecedent X.
  Y purpose P.
} => { Y a NonEmptyPurposeNode }.

#ends