PML Based AIR Justification
From TAMI
PML Based AIR Justification
Authors
Contents |
Introduction
AIR (Accountability in RDF) is an N3 based Semantic Web (Production) Rules Language. AIR rules have production rule flavor and they are executed by a forward chain AIR reasoner. AIR reasoner computes the closure for input facts and input AIR-program. AIR rules are encoded as 'if <condition> then <then-action>s else <else-actions>'. The 'if' condition is defined as a graph pattern - similar to the basic graph patterns in SPARQL - that is matched with the known (input + inferred) N3 graph at the time of reasoning. The conclusion (action) can either be another graph pattern from which an N3 graph can be constructed and inferred, or a rule that is instantiated and activated. The actions can be annotated with natural language description.
When an action is effected, it is annotated and associated with the rule id, and either the matched sub-graph or a list of components assumed to be true under the closed world assumption (CWA). The default justification for an inference is constructed by recursively taking union of annotations for the actions that led to this particular inference starting from the action which added the inference. The default justification, can be unwieldy or very revealing. Therefore, AIR supports declarative mechanisms for hiding justifications of actions by certain rules.
The justification produced in the current implementation of AIR reasoner, contains sufficient information to understand the policy decisions and to debug the policies, if needed. However, some aspects such as the rule dependencies and explanation for inferences based on negation as (finite) failure can be given out with more clarity. In case of rule dependencies, not all of them are explicitly mentioned. Nested rule dependencies is correctly captured, however, when a matched graph contains a sub-graph not in the input graph, the dependency is not made explicit. In the proposed justification ontology these dependencies are made explicit, through the association with a list of antecedents. A list of variable mappings is maintained when the pattern matches a sub-graph. For the better explanation of negation as (finite) failure, in the proposed ontology, new concepts ClosingTheWorld and DataStatus have been introduced. ClosingTheWorld operation, captures the instance when negation as finite failure is enforced, and DataStatus conveys that no match for the pattern was found under the closed world assumption.
In this work we present a PML based AIR justification ontoloy, that addresses the issues listed above. First we introduce the justification ontology in Section 2. Then we describe the vocabulary terms in detail in Section 3. In Section 4 we cover two examples.
Prefix Namespace mappings
@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 pmlp: <http://inferenceweb.stanford.edu/2006/06/pml-provenance.owl#> . @prefix pmlj: <http://inferenceweb.stanford.edu/2006/06/pml-justification.owl#> . @prefix pmll: <http://tw.rpi.edu/proj/tami.wiki/images/d/da/Pml-lite.owl#> . @prefix air: <http://dig.csail.mit.edu/2009/AIR/air#> . @prefix airj: <http://dig.csail.mit.edu/2009/AIR/airjustification#> .
Vocabulary
AIR justification ontology is based on the PML ontology. PML v2.0 ontology has 3 modules for provenance, justification and trust representations. The PML-Lite ontology describes a subset of PML concepts, in easy to understand vocabulary with a flatter structure than PML. PML-Lite vocabulary is targeted for provenance representation of common information manipulation and data flow operations. It is designed as event modeling ontology, and therefore it fits better to our needs for representing AIR justiifcation.
The AIR justification ontology shown in figure 1, is a PML-Lite based ontology. The vocabulary terms are described below. Please note that (pmll:Event pmlj:NodeSet), (pmll:Operation pmlj:InferenceRule), (pmll:operation pmlj:hasInferenceRule), (pmll:outputdata pmlj:conclusion), (pmll:inputdata [ owl:propertyChainAxiom (pmlj:antedendent pmlj:conclusion) ] ), (pmll:antecedent pmlj:antecedentList) are pairwise similar, often equivalent. Certain concepts are not represented in PML-Lite. We use PML vocabulary when it so happens.
Classes
- pmll:Event
- airj:BuiltinAssertion (rdfs:subClassOf pmll:Event)
- airj:ClosingTheWorld (rdfs:subClassOf pmll:Event)
- airj:ClosureComputation (rdfs:subClassOf pmll:Event)
- airj:Dereference (rdfs:subClassOf pmll:Event)
- airj:Extraction (rdfs:subClassOf pmll:Event)
- airj:BuiltinExtraction (rdfs:subClassOf airj:Extraction)
- airj:RuleApplication (rdfs:subClassOf pmll:Event)
- pmlj:Mapping
- pmll:Operation
- air:Rule
Properties
- pmll:antecedent
- airj:dataDependency (rdfs:subPropertyOf pmll:antecedent)
- airj:flowDependency (rdfs:subPropertyOf pmll:antecedent)
- airj:nestedDependency (rdfs:subPropertyOf airj:flowDependency)
- pmlj:conclusion
- pmll:outputdata (rdfs:subPropertyOf pmlj:conclusion)
- air:description
- airj:branch
- pmll:inputdata
- pmlj:mapFrom
- pmlj:mapTo
- air:matchedGraph
- pmll:operation
- airj:builtin
- air:rule
- pmlp:source
- pmlj:variableMappingList
- airj:inputVariableMappingList (rdfs:subPropertyOf pmll:variableMappingList)
- airj:outputVariableMappingList (rdfs:subPropertyOf pmll:variableMappingList)
- airj:outputVariableMappingListOf (inverse of airj:outputVariableMappingList)
Characteristics of Properties
- Functional Properties
- pmlj:inputVariableMappingList
- pmlj:outputVariableMappingList
- pmlj:outputdata
- air:rule
- Transitive Properties
- airj:dataDependency
- airj:flowDependency
Ontology Design
The steps of AIR reasoning are captured through following pmll:Events : airj:ClosureComputation, airj:Dereference, airj:BuiltinAssertions, airj:Extraction, airj:ClosingTheWorld and airj:RuleApplication. Figure to the right gives an overview of how these events may be annotated. Below we describe each of these events.
Closure Computation
The AIR reasoner computes the closure of input facts and AIR program. All other events described later are in some sense part of some airj:ClosureComputation event. This event is related to input facts and rules via airj:inputdata property, and to the inferred triples via the pmll:outputdata property.
Derefernce
N3, RDF or AIR documents are dereferenced to retrieve the N3 (graph) representation. The airj:Dereference event captures this operation and the source files are referred to by the pmlp:source property. The output of this operation is the N3 graph in the document.
BuiltinAssertions
Other than the given inputs there are some other N3 triples that are known to be tautologically true. Many of these are built-in assertions. In practice, built-in assertions are handled specially and created dynamically as per requirement. However we abstract this process and represent it through airj:BuiltinAssertions and airj:BuiltinExtraction events. The output of airj:BuiltinAssertions event is left implicit and is assumed to be the graph that contains all the true built-in assertions (potentially unbound) for the built-in declared using the airj:builtin property. Then assertions that are needed at the time of reasoning are extracted from the output of the corresponding airj:BuiltinAssertions event, represented as an airj:BuiltinExtraction event. The input to airj:BuiltinExtraction is left implicit, but it is related to the airj:BuiltinAssertions event via the airj:dataDependency property.
Extraction
airj:Extraction event represents the operation of getting a sub-graph (outputdata) of an N3 graph (inputdata).
Closing The World
The airj:ClosingTheWorld event refers to the step of reasoning where the triples other than the ones in input or inferred so far, and rules other than those that are active are not believed. Once the world is closed the conditions of active rules that are not satisfied are assumed to be false and all the failed rules are fired. A airj:ClosingTheWorld event event has data and/ or flow control dependencies on all the prior airj:RuleApplication events. These dependencies are represented through airj:dataDependency or airj:flowDependency properties.
Rule Application
The RuleApplication event represents a rule firing event. It is linked to the rule that fired by the air:rule property. When a nested rule is activated the known variable bindings are also passed over. Then the airj:RuleApplication event for the nested rule (say child-fire-event) has a special flow dependency, referred by airj:nestedDependency, over the airj:RuleApplication event where it's parent rule fired (say parent-fire-event). The input variable bindings for child-fire-event is implicit and is same as the output variable bindings of the parent-fire-event. Please note that airj:nestedDependency is non transitive. When the condition of the rule is satisfied new variable bindings may be acquired and the then-actions are effected. Otherwise, the else-actions are effected. Which actions are affected is declared using the air:branch property. The variable bindings are acquired upon pattern matching of the rule condition against the fact base, and the matched graph is declared through airj:matchedgraph property. The variable bindings can be deduced from the matched graph and the condition. Alternatively they can be explicitly asserted using the airj:outputVariableMappingList property. The triples asserted when the rule fired is declared using the airj:outputdata property. The airj:nestedDepedency relationship between airj:RuleApplication events captures activation of a rule, as described before. The event is annotated with natural language description by air:description property. The airj:RuleApplication events also have data dependencies on other events. The condition can be satisfied by triples from more than one input logs, or by triples asserted in some of the prior airj:RuleApplication events. These events also have flow control dependencies over prior airj:ClosingTheWorld events.
Ellipsed & Hidden Justifications
The design discussed so far covers what the default justification would look like. It differs for hidden and ellipsed rules, as described below. No new vocabulary is needed as such, but existentially quantified variables are used to allude to the existence of airj:RuleApplication events while hiding the details of these events.
Ellipsed Justification
If a rule (hence any instance of the rule) is typed as air:Ellipsed-rule, then, in the justification only the flow control related information is provided for the RuleApplication events of this rule. All other details are suppressed.
Hidden Justification
If a rule (or an instance of rule) is typed as air:Hidden-rule, then, in the justification the nested structure beyond this rule is hidden. All 'air:Actions effected in this rule or any of the child rules are shown to be effected from a single RuleApplication event. Other details, except for partial flow control information, is suppressed.
Examples
The first example is an abstract one and it uses airj:matchedgraph to capture the acquired bindings, where as the second example uses airj:outputVariableMappingList to capture the same.
Example 1 : Abstract Example (covers all justification ontology features)
We'll consider an example that covers following scenarios :
- dependency on inferred graph for a policy decision
- 'then' 'air:(non-)compliant-with' property assertion
- 'else' 'air:(non-)compliant-with' property assertion
- ellipsed justifications (after re-typing a rule)
- hidden justifications (after re-typing a rule)
AIR-program
@prefix : <http://dig.csail.mit.edu/TAMI/2007/cwmrete/nonce#> .
@prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .
@forAll :var1 .
:ExamplePolicy a air:Policy;
air:rule :Rule1;
air:rule :Rule2.
:Rule1 a air:Belief-rule;
air:label "Rule 1";
air:if {};
air:then [ air:assert [ air:statement {:s1 :p :o .
:s2 :p :o . } ] ].
:Rule2 a air:Belief-rule;
air:label "Rule 2";
rdfs:comment "Introduce another level of nesting";
air:if {};
air:then [ air:rule :Rule21 ] .
:Rule21 a air:Belief-rule;
air:label "Rule 2";
air:if {:var1 :p :o .
:var1 :assertedp :o .
(1 2) math:sum 3 . };
air:then [ air:description (:var1 "satisfies the first set of checks");
air:rule :Rule211] .
:Rule211 a air:Belief-rule;
air:label "Rule211";
air:if {:var1 :assertedp :o1 .};
air:then [air:assert [air:statement {:var1 air:compliant-with :ExamplePolicy}]];
air:else [air:assert [air:statement {:var1 air:non-compliant-with :ExamplePolicy}]].
Log
@prefix : <http://dig.csail.mit.edu/TAMI/2007/cwmrete/nonce#> . :s1 :assertedp :o; :assertedp :o1. :s2 :assertedp :o.
Justifications
Default Justification
@prefix : <http://dig.csail.mit.edu/TAMI/2007/cwmrete/nonce#> .
@prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .
@prefix tms: <http://dig.csail.mit.edu/TAMI/2007/amord/tms#> .
@prefix pmlj: <http://.../PML-Justification>
@prefix pmlp: <http://.../PML-Provenance>
@prefix pmll: <http://.../PML-LITE>
@prefix airj: <http://.../AIR-Justification>
@prefix pr: <http://.../proof>
pr:deref-log a airj:Dereference ;
pmlp:source <log-uri> ;
pmll:outputdata pr:log .
pr:deref-rules a airj:Dereference ;
pmlp:source <rules-uri> ;
pmll:outputdata pr:prog .
pr:MainEvent a airj:ClosureComputation ;
pmll:outputdata { :s1 air:compliant-with :ExamplePolicy .
:s2 air:non-compliant-with :ExamplePolicy . };
pmll:inputdata pr:log, pr:prog .
pr:Event1 a airj:RuleApplication;
airj:matchedgraph {} ;
pmll:outputdata {:s1 :p :o .
:s2 :p :o . };
air:rule :Rule1 ;
airj:branch air:then .
pr:Event2 a airj:RuleApplication;
airj:matchedgraph {} ;
air:rule :Rule2 ;
airj:branch air:then.
pr:math a airj:BuiltinAssertions ;
airj:builtin math:sum .
pr:math-1 a airj:BuiltinExtraction ;
airj:dataDependency pr:math ;
pmll:outputdata { (1 2) math:sum 3 . } .
pr:Event3_1 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s1 :p :o .
:s1 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s1 satisfies the first set of checks" ;
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
pr:Event3_2 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s2 :p :o .
:s2 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s2 satisfies the first set of checks";
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
pr:Event4 a airj:RuleApplication;
pmll:outputdata {:s1 air:compliant-with :ExamplePolicy . };
air:rule :Rule211;
airj:nestedDependency pr:Event3_1 ;
airj:matchedgraph {:s1 :assertedp :o1 .};
airj:branch air:then ;
airj:dataDependency pr:deref-log .
pr:Event5 a airj:ClosingTheWorld;
pmll:flowDependency pr:deref-log, pr:Event1, pr:Event4;
pmll:dataDependency pr:deref-log, pr:Event1, pr:Event4.
pr:Event6 a pmll:RuleApplication;
pmll:outputdata { :s2 air:non-compliant-with :ExamplePolicy . };
air:rule :Rule211;
airj:nestedDependency pr:Event3_2 ;
airj:flowDependency pr:Event5 ;
airj:branch air:else ;
airj:dataDependency pr:Event5 .
Ellipsed Justification
We will now modify the example policy and type :Rule21 as an Ellipsed Rule. This will affect the default justification, so that part of the description of pr:Event3_1 (and pr:Event3_2) are hidden. The difference in the two justifications is shown below:
:Rule21 a air:Belief-rule
pr:Event3_1 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s1 :p :o .
:s1 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s1 satisfies the first set of checks" ;
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
pr:Event3_2 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s2 :p :o .
:s2 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s2 satisfies the first set of checks";
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
:Rule21 a air:Ellipsed-rule
@forSome pr:Event3_1.
pr:Event3_1 a airj:RuleApplication;
airj:nestedDependency pr:Event2;
air:description ":s1 satisfies the first set of checks".
@forSome pr:Event3_2.
pr:Event3_2 a airj:RuleApplication;
airj:nestedDependency pr:Event2;
air:description ":s2 satisfies the first set of checks".
Hidden Justification
If now :Rule21 is typed as a Hidden Rule, it will affect the default justification. The nested structured and some other details will be hidden now. The difference in the two justifications is shown below :
:Rule21 a air:Belief-rule
pr:math a airj:BuiltinAssertions ;
airj:builtin math:sum .
pr:math-1 a airj:BuiltinExtraction ;
airj:dataDependency pr:math ;
pmll:outputdata { (1 2) math:sum 3 . } .
pr:Event3_1 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s1 :p :o .
:s1 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s1 satisfies the first set of checks" ;
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
pr:Event3_2 a airj:RuleApplication;
air:rule :Rule21;
airj:nestedDependency pr:Event2;
airj:matchedgraph {:s2 :p :o .
:s2 :assertedp :o .
(1 2) math:sum 3 . };
airj:branch air:then;
air:description ":s2 satisfies the first set of checks";
airj:dataDependency pr:deref-log, pr:Event1, pr:math-1 .
pr:Event4 a airj:RuleApplication;
pmll:outputdata {:s1 air:compliant-with :ExamplePolicy . };
air:rule :Rule211;
airj:nestedDependency pr:Event3_1 ;
airj:matchedgraph {:s1 :assertedp :o1 .};
airj:branch air:then ;
airj:dataDependency pr:deref-log .
pr:Event5 a airj:ClosingTheWorld;
pmll:flowDependency pr:deref-log, pr:Event1, pr:Event4;
pmll:dataDependency pr:deref-log, pr:Event1, pr:Event4.
pr:Event6 a pmll:RuleApplication;
pmll:outputdata { :s2 air:non-compliant-with :ExamplePolicy . };
air:rule :Rule211;
airj:nestedDependency pr:Event3_2 ;
airj:flowDependency pr:Event5 ;
airj:branch air:else ;
airj:dataDependency pr:Event5 .
:Rule21 a air:Hidden-rule
@forSome pr:Event3_1.
pr:Event3_1 a airj:RuleApplication;
pmll:outputdata {:s1 air:compliant-with :ExamplePolicy . };
airj:nestedDependency pr:Event2.
@forSome pr:Event3_2.
pr:Event3_2 a airj:RuleApplication;
pmll:outputdata {:s2 air:compliant-with :ExamplePolicy . };
airj:nestedDependency pr:Event2.
Example 2 : Copyright Violation
Policy
@forAll :Violation, :Work, :Creator, :ViolationDate, :DeathDate .
:CopyrightCriminalPolicy a air:Policy ;
air:rule :FindInfringement .
:FindInfringement a air:Belief-rule ;
air:if { :Violation a copyright:PotentialCopyrightInfringement ;
copyright:infringesCopyrightOn :Work . } ;
air:then [ air:rule :FindValue ] .
:FindValue a air:Belief-rule ;
air:if { :Work gr:hasCurrencyValue :Value ;
gr:hasCurrency "USD" . } ;
air:then [ air:rule :CheckValue ] .
:CheckValue a air:Beliefrule;
air:if { :Value math:notLessThan "1000" . } ;
air:else [ air:assert { :Violation air:non-compliant-with :CopyrightCriminalPolicy . } ;
air:description ( :Violation " is not a criminal copyright infringement as it is under $1,000 in value" ) ] .
Log
:MinorInfringement a copyright:PotentialCopyrightInfringement ;
copyright:infringesCopyrightOn :SpaceOdyssey ;
copyright:infringementDate "20081001" .
:SpaceOdyssey a movie ;
gr:hasCurrencyValue "30" ;
gr:hasCurrency "USD" ;
dc:creator :StanleyKubrick .
"30" math:lessThan "1000" .*
* - consider this fact to be a premise
Justifications
Default Justification
pr:inputLog is log:semantics of <http://dig.csail.mit.edu/TAMI/inprogress/examplelog.n3>.
pr:GetDataLog a airj:Extraction;
pmll:outputdata pr:inputLog.
pr:Event4 a airj:RuleApplication ;
air:rule :CheckValue ;
pmll:outputdata { :MinorInfringement air:non-compliant-with :CopyrightCriminalPolicy . } ;
air:description ":MinorInfringement is not a criminal copyright infringement as it is under $1,000 in value" ;
airj:branch air:else ;
airj:dataDependency pr:ClosingTheWorld-1 ;
airj:flowDependency pr:Event3, pr:ClosingTheWorld-1 .
pr:ClosingTheWorld-1 a airj:ClosingTheWorld ;
pmll:flowDependency pr:GetDataLog, pr:Event3 ;
pmll:dataDependency pr:GetDataLog .
pr:Event3 a airj:RuleApplication ;
air:rule :FindValue ;
airj:outputVariableMappingList (pr:Mapping3, pr:Mapping2, pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog ;
airj:flowDependency pr:Event2 .
pr:Event2 a airj:RuleApplication ;
air:rule :FindInfringement ;
airj:outputVariableMappingList (pr:Mapping2, pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog ;
airj:flowDependency pr:Event1 .
pr:Event1 a airj:RuleApplication ;
air:rule :CopyrightCriminalPolicy ;
airj:outputVariableMappingList (pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog .
pr:Mapping3 a pmlj:Mapping;
pmlj:mappingFrom :Value;
pmlj:mappingTo “30”.
pr:Mapping2 a pmlj:Mapping;
pmlj:mappingFrom :Work;
pmlj:mappingTo :SpaceOdyssey.
pr:Mapping1 a pmlj:Mapping;
pmlj:mappingFrom :Violation;
pmlj:mappingTo :MinorInfringement.
:FindValue a air:Ellipsed-rule
pr:Event4 a airj:RuleApplication ;
air:rule :CheckValue ;
pmll:outputdata { :MinorInfringement air:non-compliant-with :CopyrightCriminalPolicy . } ;
air:description ":MinorInfringement is not a criminal copyright infringement as it is under $1,000 in value" ;
airj:branch air:else ;
airj:dataDependency pr:ClosingTheWorld-1 ;
airj:flowDependency pr:Event3, pr:ClosingTheWorld-1 .
pr:ClosingTheWorld-1 a airj:ClosingTheWorld ;
pmll:flowDependency pr:GetDataLog, pr:Event3 ;
pmll:dataDependency pr:GetDataLog .
@forSome pr:Event3 .
pr:Event3 a airj:RuleApplication ;
airj:flowDependency pr:Event2 . # Other details have been suppressed.
pr:Event2 a airj:RuleApplication ;
air:rule :FindInfringement ;
airj:outputVariableMappingList (pr:Mapping2, pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog ;
airj:flowDependency pr:Event1 .
pr:Event1 a airj:RuleApplication ;
air:rule :CopyrightCriminalPolicy ;
airj:outputVariableMappingList (pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog .
pr:Mapping2 a pmlj:Mapping;
pmlj:mappingFrom :Work;
pmlj:mappingTo :SpaceOdyssey.
pr:Mapping1 a pmlj:Mapping;
pmlj:mappingFrom :Violation;
pmlj:mappingTo :MinorInfringement.
:FindValue a air:Hidden-rule
pr:Event4 a airj:RuleApplication ;
pmll:outputdata { :MinorInfringement air:non-compliant-with :CopyrightCriminalPolicy . } ;
air:description ":MinorInfringement is not a criminal copyright infringement as it is under $1,000 in value" ;
airj:flowDependency pr:Event2 . # All the nesting after the:FindValue rule has been suppressed.
pr:Event2 a airj:RuleApplication ;
air:rule :FindInfringement ;
airj:outputVariableMappingList (pr:Mapping2, pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog ;
airj:flowDependency pr:Event1 .
pr:Event1 a airj:RuleApplication ;
air:rule :CopyrightCriminalPolicy ;
airj:outputVariableMappingList (pr:Mapping1) ;
airj:branch air:then ;
airj:dataDependency pr:GetDataLog .
pr:Mapping2 a pmlj:Mapping;
pmlj:mappingFrom :Work;
pmlj:mappingTo :SpaceOdyssey.
pr:Mapping1 a pmlj:Mapping;
pmlj:mappingFrom :Violation;
pmlj:mappingTo :MinorInfringement.
Builtins
1. log:semantics mapped to event airj:Dereference
- [] a airj:Dereference ;
- pmlp:Source <log-uri> .
2. data-dependency over airj:BuiltinExtraction
- [] a airj:BuiltinExtraction ;
- pmll:outputdata { (1 2) math:sum 3 } ;
- airj:dataDependency :mathbltn .
- :mathbilt a airj:BuiltinAssertions ;
- airj:builtin math:sum .
2.1. Alternatively # Skeptical about referring to an unbound graph by URI
- [] a airj:BuiltinExtraction ;
- pmll:outputdata { (1 2) math:sum 3 } ;
- inputdata :mathbltngraph .
- airj:dataDependency :mathbltn .
- :mathbltn a airj:BuiltinAssertions ;
- airj:builtin math:sum ;
- airj:outputdata :mathbltngraph .
Inference Rules on Justification
For rules responsible for an assertion
We may want to know what rules are responsible for an assertion. We consider three kinds of responsibilities. First, the rule which made the assertion is responsible. Second, another rule triggers the rule which made the assertion, then former is considered responsible. Third, another rule asserts triple(s) which helps satisfying the condition of the rule and triggering the assertion, then the former rule is considered responsible. We coin a new vocabulary airj:impacts with domain and range :RuleApplication. :Event1 :impacts :Event2 in two ways. First when :Event2 has :dataDependency or :nestedDependency on :Event1. Second, when :Event2 is :impacted by another :Event which has :dataDependency or :nestedDependency on :Event1. In the second case we require that :Event2 make some assertion, because an impact relationship to some Event where no assertion has been made is seldom interesting. Note that we ignore data and flow dependencies on :ClosingTheWorld events and more data and flow depencies from there.
:ImpactRelationshipsBwEvents a air:RuleSet ;
air:rule :dataDependencyBwEvents,
:nestedDependencyBwEvents .
:dataDependencyBwEvents a air:BeliefRule ;
air:if { ?Event2 a air:RuleApplication ;
airj:dataDependency ?Event1 .
?Event1 a airj:RuleApplication } ;
air:then [ air:assert {?Event1 airj:impacts ?Event2 } ] ,
[ air:rule :impactsClosureToLeaves ] .
:nestedDependencyBwEvents a air:BeliefRule ;
air:if { ?Event2 a air:RuleApplication ;
airj:nestedDependency ?Event1 .
?Event1 a airj:RuleApplication } ;
air:then [ air:assert {?Event1 airj:impacts ?Event2 } ] ,
[ air:rule :impactsClosureToLeaves ] .
:impactsClosureToLeaves a air:BeliefRule ;
air:if { @forSome :Data .
?Event2 airj:impacts ?Event3 .
?Event3 a airj:RuleApplication ;
airj:outputdata :Data } ;
air:then [ air:assert {?Event1 airj:impacts ?Event3 } ] .
References
- PML Lite - internal
- PML v 2.0
- CWM Proof and PML - Translating CWM Proof into PML
