# $Author: lkagal $
# $Date: 2006-06-23 17:59:34 -0400 (Fri, 23 Jun 2006) $
# $Revision: 743 $

# USAGE: cwm rules.n3 --think  --filter="min-filter.n3"
# USAGE: cwm rules.n3 --think  --filter="filter.n3"

# USAGE to generate proof : cwm rules.n3 --think --filter="min-filter.n3" --base=foo --why > 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, F, G.
@forAll P, A, C, R, S.

{ (<http://dig.csail.mit.edu/TAMI/cph/v2/data.ttl>.log:semantics
   <http://dig.csail.mit.edu/TAMI/cph/v2/background.ttl>.log:semantics 
  ) log:conjunction G.
} => { G a TamiData }.

# identifying proof tree
{ G a TamiData.
  G log:includes { X a j:Arrest }.
} => { X a ProofNode }.

{ X a ProofNode.
  G a TamiData.
  G log:includes { X ts:antecedent Y }.
} => { Y a ProofNode }.

{ X a ProofNode.
  G a TamiData.
  G log:includes { X ts:antecedent tb:no-antecedent }.
} => { X a RootNode. }.

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

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

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


#ends